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 41 to 60 of 1,644 declarations.
lemma
bound_f_second_term
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1198
lemma
bound_f_first_term
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1228
lemma
smaller_terms
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1274
lemma
second_smaller_terms
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1303
lemma
x_log_x_atTop
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1332
lemma
tendsto_by_squeeze
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1351
theorem
prime_between
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1546
theorem
sum_mobius_div_self_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1576
lemma
sum_mobius_mul_floor
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1647
lemma
sum_mu_Lambda
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1678
lemma
M_log_identity
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1693
lemma
sum_mobius_div_isBigO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1730
lemma
sum_log_div_isBigO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1741
lemma
R_locally_bounded
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1763
lemma
sum_bounded_of_linear_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1780
lemma
sum_abs_R_isLittleO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1806
lemma
R_linear_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1846
lemma
M_isLittleO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1857
theorem
mu_pnt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1923
lemma
lambda_eq_sum_sq_dvd_mu
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1973
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.