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 381 to 400 of 1,644 declarations.
theorem
FKS2.dawson_le_sharp
Sharp Dawson upper bound: for 0 ≤ w ≤ z,
dawson z ≤ 1/(2z) + e^{w²}/(4z³) + (z−w)·e^{−w(2z−w)}.
Refines dawson x ≤ 1/x to the true leading term 1/(2z) with explicitly
controlled corrections; a moderate w makes the last two terms negligible
for large z. This is the estimate behind the numerical bound on
μ_asymp in Corollary 22.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:401
lemma
FKS2.F_strictAnti
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:469
lemma
FKS2.dawson_lt_S6
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:521
lemma
FKS2.S5_lt_dawson
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:560
theorem
FKS2.remark_after_corollary_11
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:652
lemma
FKS2.two_mul_sqrt_div_le_quarter
Key inequality behind the exponential decay:
for t ≥ 1000 we have 2 * sqrt (t/R) ≤ t/4 with R = 5.5666305.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:704
lemma
FKS2.BKLNW_a1_le_two_of_ge_1000
A very crude upper bound on BKLNW.a₁ at large t.
You can make this as weak as you like; ≤ 2 is plenty.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:739
lemma
FKS2.BKLNW_a2_le_five_mul_of_ge_1000
A crude linear bound on BKLNW.a₂ at large t.
Any linear bound is enough; ≤ 5*t is extremely safe for t ≥ 1000.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:775
lemma
FKS2.sixty_thousand_mul_exp_neg_230_le
Purely numerical tail bound used at the end:
60000 * exp (-230) ≤ 1e-5.
This can be discharged by interval_decide.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:891
lemma
FKS2.t_mul_exp_neg_one_thousandth_le_five_hundred
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:902
lemma
FKS2.exp_neg_five_twelfths_mul_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:924
lemma
FKS2.part1_decay_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:946
lemma
FKS2.part2_decay_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:977
theorem
FKS2.nu_asymp_le_remark_15_margin
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1078
theorem
FKS2.proposition_13
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1220
lemma
FKS2.corollary_14_small_adm
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1382
theorem
FKS2.corollary_14
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1635
theorem
FKS2.remark_15'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1722
theorem
FKS2.remark_15
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1802
theorem
FKS2.Li_identity
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:1835
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.