Head version
a93551347dce
a93551347dce924b1db75d40218841bf085a465f
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 22 Jul 2026
- Dependencies
- 13
- Versions
- 9
All packages
AlexKontorovich/PrimeNumberTheoremAnd
PrimeNumberTheoremAnd
Blueprint for the PNT+ Project
Therefore indexed 1,644 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
External build observation
Exact head commit and toolchain
No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.
Pin this source in lakefile.lean
require PrimeNumberTheoremAnd from git "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git" @ "a93551347dce924b1db75d40218841bf085a465f"
Source declarations
1,644 indexed proofs
Showing 941 to 960 of 1,644 declarations.
lemma
ArithmeticFunction.sum_moebius_sq_divisors_IsMultiplicative
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1295
lemma
ArithmeticFunction.sum_moebius_sq_divisors_apply_prime_pow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1325
lemma
ArithmeticFunction.moebius_sq_eq
I-K (1.33): μ^2(n) = ∑ d^2|n μ(d).
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1364
theorem
continuous_laplaceIntegral_verticalLine_of_integrable
Continuity of the bilateral Laplace integral along a vertical line, under integrability of the exponentially weighted source on that line.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:33
theorem
laplaceTransformBilateral_eq_fourier
On a vertical line, the bilateral Laplace transform is the Fourier transform of the exponentially weighted function.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:100
theorem
fourierInvTrunc_fourier_eq_integral_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:125
theorem
integrable_truncated_fourier_kernel_prod
The truncated oscillatory Fourier kernel is product-integrable when the source is integrable. This is the finite-height Fubini input for principal-value inversion.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:152
theorem
fourierInvTrunc_fourier_eq_integral_kernel
Fubini swaps the finite-height inverse Fourier integral into the standard
Dirichlet-kernel form. The hypothesis 0 ≤ T is the only orientation condition
needed for the interval integral.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:172
theorem
integral_exp_mul_I_scaled_of_ne
Scaled finite-height exponential integral, away from zero frequency.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:188
theorem
normalized_sinc_smul_eq_sin_div
The normalized sinc kernel is the usual sin (T * u) / (π * u) kernel,
with the removable value at u = 0 made explicit.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:291
lemma
tendsto_div_two_pi_atTop_cocompact
The scaled positive-frequency ray T / (2π) tends to the cocompact filter.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:347
lemma
tendsto_neg_div_two_pi_atTop_cocompact
The scaled negative-frequency ray -T / (2π) tends to the cocompact filter.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:361
lemma
integrable_exp_neg_mul_I_smul
Multiplying an integrable function by a negative unit-modulus exponential preserves integrability.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:413
theorem
tendsto_integral_sin_mul_smul_atTop
Riemann-Lebesgue in sine-integral form. This is the oscillatory cancellation brick used by the non-L1 principal-value Laplace inversion route.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:439
theorem
local_quotient_eq_dslope
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:487
theorem
intervalIntegrable_local_quotient_of_differentiableAt
Differentiability at the target point makes the local sine-error quotient interval-integrable on every positive window.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:512
theorem
intervalIntegrable_sin_div_kernel_error_of_intervalIntegrable_quotient
Local quotient integrability gives interval-integrability of the finite sine-kernel error term.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:546
theorem
tendsto_intervalIntegral_sin_div_kernel_error_of_intervalIntegrable_quotient
Local quotient integrability gives the finite-window Riemann-Lebesgue cancellation for the sine-kernel error term.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:571
theorem
norm_sin_div_kernel_le_abs_height
The removable sine kernel is bounded by its height.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:612
theorem
integrable_sin_div_kernel_smul_of_integrable
The sine kernel times an integrable source remains integrable.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:633
Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.