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,521 to 1,540 of 1,644 declarations.
theorem
decay_bounds_W21
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:407
lemma
W21.integrable_fourier
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:462
lemma
summation_by_parts
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:595
lemma
BoundedAtFilter.comp_add
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:640
lemma
summable_iff_bounded'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:650
lemma
exists_antitone_of_eventually
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:680
lemma
summable_inv_mul_log_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:696
lemma
log_mul_add_isBigO_log
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:734
lemma
Asymptotics.IsBigO.add_isLittleO_right
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:762
lemma
log_add_one_sub_log_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:789
lemma
nnabla_mul_log_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:812
theorem
limiting_fourier_lim1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:974
theorem
limiting_fourier_lim2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1005
theorem
limiting_fourier_lim3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1060
lemma
limiting_fourier
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1109
lemma
hh_deriv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1276
lemma
gg_le_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1317
lemma
cancel_main'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1394
theorem
sum_le_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1404
lemma
bound_sum_log
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1547
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.