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,541 to 1,560 of 1,644 declarations.
lemma
bound_sum_log0
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1626
lemma
summable_fourier
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1652
lemma
bound_I1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1660
lemma
bound_I2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1682
lemma
limiting_cor_W21
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1718
theorem
wiener_ikehara_smooth_sub
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1900
lemma
wiener_ikehara_smooth
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1944
lemma
wiener_ikehara_smooth_real
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2032
lemma
interval_approx_inf
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2048
lemma
interval_approx_sup
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2082
lemma
WI_sum_Iab_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2128
theorem
residue_nonneg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2198
lemma
WienerIkeharaInterval
Now we add the hypothesis that for all .
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2226
lemma
tendsto_mul_ceil_div
A version of the Wiener-Ikehara Tauberian Theorem: If f is a nonnegative arithmetic
function whose L-series has a simple pole at s = 1 with residue A and otherwise extends
continuously to the closed half-plane re s ≥ 1, then ∑ n < N, f n is asymptotic to A*N.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2346
lemma
S_sub_S
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2363
lemma
tendsto_S_S_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2375
theorem
WienerIkeharaTheorem'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2392
theorem
WeakPNT
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2438
theorem
limiting_fourier_lim2_gt_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2503
theorem
limiting_fourier_lim3_gt_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:2543
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.