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 21 to 40 of 1,644 declarations.
theorem
BrunTitchmarsh.card_range_filter_isPrimePow_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:507
lemma
Set.Ico_subset_Ico_of_Icc_subset_Icc
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:16
theorem
WeakPNT'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:85
theorem
WeakPNT''
An alternate form of the Weak PNT.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:105
theorem
chebyshev_asymptotic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:162
theorem
chebyshev_asymptotic_finsum
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:187
theorem
chebyshev_asymptotic'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:217
theorem
chebyshev_asymptotic''
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:247
theorem
primorial_bounds
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:278
theorem
primorial_bounds_finprod
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:301
lemma
integral_log_inv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:331
lemma
integral_log_inv_pos
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:398
lemma
integral_log_inv_pialt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:808
lemma
integral_div_log_asymptotic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:818
theorem
pi_alt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:853
lemma
pi_nth_prime_asymp
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:922
lemma
log_nth_prime_asymp
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:934
theorem
pn_asymptotic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:961
theorem
pn_pn_plus_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:997
lemma
prime_in_gap
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1179
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.