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 821 to 840 of 1,644 declarations.
theorem
log_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:36
theorem
log_ge'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:71
theorem
symm_inv_log
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:92
theorem
li.sub_Li
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:167
theorem
li.two_approx
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:202
lemma
PT.admissible_bound_weaken
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:65
lemma
PT.table_1_bounds
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:90
theorem
PT.corollary_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:101
theorem
PT.corollary_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:128
theorem
JY.corollary_1_3
results from \cite{johnston-yang}
PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:268
lemma
Buthe2.eventually_Buthe_theta_eq_theta
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:119
theorem
Dusart1999.theorem_a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:363
theorem
Dusart1999.theorem_d
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:401
theorem
Dusart.theta_improv_1
Some results from \cite{Dusart2018}
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:439
theorem
Dusart.theta_improv_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:472
theorem
FaberKadiri.psi_bound
Some results from \cite{faber-kadiri}, \cite{faber-kadiri-corrigendum}
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:495
theorem
JY.psi_bound_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:532
theorem
FKS.psi_bound
Some results from \cite{FKS}
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:601
theorem
Rosser1938.p_n_gt_1
Some results from \cite{rosser1938}
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:903
theorem
Rosser1938.p_n_gt_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:997
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.