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 61 to 80 of 1,644 declarations.
lemma
sum_lambda_eq_sum_mu_div_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2096
lemma
sum_mu_div_sq_isLittleO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2133
theorem
lambda_pnt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2201
lemma
sum_mobius_floor
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2254
lemma
sum_mobius_floor_tail_isLittleO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2264
lemma
sum_mobius_div_approx
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2352
theorem
mu_pnt_alt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2371
theorem
chebyshev_asymptotic_pnt
\section{Consequences of the PNT in arithmetic progressions}
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2436
theorem
dirichlet_thm
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2514
lemma
admissible_bound.mono
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Defs · PrimeNumberTheoremAnd/Defs.lean:198
lemma
Eψ.classicalBound.to_numericalBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Defs · PrimeNumberTheoremAnd/Defs.lean:258
lemma
Eθ.classicalBound.to_numericalBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Defs · PrimeNumberTheoremAnd/Defs.lean:280
lemma
Eπ.classicalBound.to_numericalBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Defs · PrimeNumberTheoremAnd/Defs.lean:293
lemma
integral_deriv_mul_add_const
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:28
lemma
intervalIntegrable_deriv_mul_B1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:41
lemma
integral_deriv_mul_floor_add_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:51
theorem
sum_eq_integral_add_integral_deriv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:67
lemma
eulerMascheroniSeq_diff_lb
For m ≥ n, the difference of Euler-Mascheroni sequence values is bounded below
by a telescoping sum.
PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:82
lemma
eulerMascheroniConstant_lb
γ ≥ γ₁(n+1) for all n.
PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:99
lemma
euler_maclaurin_decreasing
γ₂ is strictly decreasing for n ≥ 1.
PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:186
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.