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 1,201 to 1,220 of 1,644 declarations.
lemma
Real.dyadicShell_upper_bound
If k = ⌊log₂ (x / r₀)⌋, then x is bounded by the next dyadic endpoint.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:66
lemma
Real.one_le_dyadicRadius_succ_of_inv_le_two_pow
Once the dyadic scale is past r₀⁻¹, the upper endpoint r₀ 2^(k+1) is at least 1.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:89
lemma
Real.one_add_abs_two_mul_dyadicRadius_rpow_le
A dyadic radius r₀ 2^(k+1) gives polynomial growth bounded by a geometric term.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:108
lemma
Real.tsum_inv_rpow_le_card_mul_of_lower_bound
A finite shell whose radii are bounded below contributes at most
card * lower_radius⁻¹ ^ τ to the inverse-power sum.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:178
lemma
Real.inv_dyadicRadius_rpow_eq
Inverse powers of dyadic radii split into the initial radius and a geometric factor.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:192
lemma
Real.dyadic_trailing_inv_term_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:248
lemma
Real.dyadic_growth_mass_mul_inv_le_geometric
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:264
theorem
Real.log_two_le_log_two_mul_mul_inv_norm_of_norm_le
If z ≠ 0 and ‖z‖ ≤ R, then log 2 ≤ log (2R * ‖z‖⁻¹).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:66
theorem
Real.norm_le_exp_mul_rpow_of_log_growth
A logarithmic growth bound gives a pointwise exponential norm bound after weakening the exponent.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:86
theorem
Real.log_growth_of_norm_le_exp_mul_rpow
Convert a pointwise exponential norm bound into a logarithmic growth bound.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:97
theorem
Real.exists_norm_le_exp_mul_pow_of_rpow_bound
A pointwise exponential bound with real exponent can be weakened to a natural exponent.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:115
theorem
Real.sq_le_exp_const_mul_rpow
A quadratic polynomial factor is absorbed by any positive exponential rpow margin.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:130
theorem
Real.exp_mul_rpow_le_exp_mul_rpow_of_le_mul
A multiplicative radius comparison gives the corresponding exponential rpow comparison.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:166
theorem
Real.exists_between_self_and_floor_add_one_same_floor
A midpoint between ρ and ⌊ρ⌋ + 1 has the same natural floor as ρ.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:176
theorem
Complex.HasDerivAt.const_mul_ofReal_cpow_neg_sub_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean:46
theorem
Real.log_mul_rpow_neg_le_two_div_mul_rpow_neg
For 1 < u and ε > 0, log u * u^(-1-ε) ≤ (2/ε) * u^(-1-ε/2).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean:15
theorem
Finset.sum_Icc_one_eq_sum_range
Reindex ∑ k ∈ Icc 1 N, f k as ∑ n ∈ range N, f (n + 1).
PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation · PrimeNumberTheoremAnd/Mathlib/NumberTheory/AbelSummation.lean:25
theorem
Finset.sum_Icc_zero_eq_sum_Icc_one
If f 0 = 0, the term at 0 in Icc 0 N is redundant.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation · PrimeNumberTheoremAnd/Mathlib/NumberTheory/AbelSummation.lean:47
theorem
Chebyshev.primeFactors_lcmUpto
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Chebyshev.lean:76
theorem
Chebyshev.lcmUpto_eq_prod
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Chebyshev.lean:95
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.