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 1,561 to 1,580 of 1,644 declarations.
lemma
tendsto_tsum_of_monotone_convergence
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2573
lemma
tendsto_tsum_of_monotone_convergence_nhdsGT_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2588
lemma
limiting_fourier_variant
\section{Removing the Chebyshev hypothesis}
In this section we do not assume the bound \eqref{cheby}, but instead derive it from the other hypotheses.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2999
lemma
norm_mul_integral_Ici_le_integral_norm
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3160
lemma
integrable_norm_fourier_scaled_of_CS2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3219
lemma
exists_bound_norm_G_on_tsupport
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3280
lemma
norm_integrand_le_K_mul_norm_psi
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3304
lemma
norm_error_integral_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3329
lemma
crude_upper_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3389
lemma
Real.fourierIntegral_convolution
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3534
lemma
Real.fourierIntegral_conj_neg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3563
lemma
auto_cheby_exists_smooth_nonneg_fourier_kernel
Smooth compactly supported function with non-negative Fourier transform via self-convolution.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3580
lemma
auto_cheby_fourier_summable
The series ∑ f(n)/n · 𝓕ψ(log(n/x)/(2π)) is summable for x ≥ 1.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3630
lemma
auto_cheby_short_interval_bound
Short interval bound from global filtered bound: if ∑ f(n)/n · 𝓕ψ(log(n/x)) ≤ B,
then ∑_{(1-ε)x < n ≤ x} f(n) ≤ Cx for some ε, C > 0.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3720
lemma
auto_cheby_bootstrap_induction
Bootstraps short interval bounds to global Chebyshev bound via strong induction.
If ∑_{(1-ε)x < n ≤ x} f(n) ≤ Cx for all x ≥ 1, then ∑_{n ≤ x} f(n) = O(x).
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3803
lemma
auto_cheby
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3873
theorem
WeakPNT_character
\section{The prime number theorem in arithmetic progressions}
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3912
theorem
WeakPNT_AP_prelim
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3951
lemma
summable_vonMangoldt_div_rpow
The von Mangoldt function divided by n ^ s is summable for s > 1.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:3990
theorem
WeakPNT_AP
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:4012
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.