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,181 to 1,200 of 1,644 declarations.
theorem
Complex.Gamma.norm_le_Gamma_re
The Euler integral gives ‖Γ z‖ ≤ Γ (re z) for 0 < re z; compare [DLMF], §5.2.1.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/IntegralBounds.lean:61
lemma
Real.Stirling.log_three_le_coef_mul_log_one_add
For x ≥ 1, log 3 ≤ (log 3 / log 2) * log (1 + x).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:71
lemma
Real.Stirling.half_shift_log_constant_pos
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:87
lemma
Complex.Gamma.log_one_add_norm_add_one_le
For ‖s‖ ≥ 1, log(1 + ‖s + 1‖) ≤ log 2 + log(1 + ‖s‖).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:117
lemma
Complex.Gamma.log_one_add_norm_div_two_add_one_le
For ‖s‖ ≥ 1, log(1 + ‖s/2 + 1‖) ≤ log 3 + log(1 + ‖s‖).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:132
lemma
Complex.Gamma.norm_mul_log_shift_add_one_bound
For ‖s‖ ≥ 1, the s ↦ s + 1 shift in the Stirling exponent is absorbed by a factor 4.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:146
lemma
Complex.Gamma.norm_mul_log_shift_half_bound
For ‖s‖ ≥ 1, the s ↦ s/2 + 1 shift in the half-plane Stirling exponent.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:162
lemma
Complex.Gamma.norm_Gamma_le_two_mul_norm_Gamma_add_one
From Γ(z + 1) = z Γ(z) and 1/2 ≤ ‖z‖, bound ‖Γ(z)‖ by 2 * ‖Γ(z + 1)‖.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:188
theorem
Complex.Gamma.norm_bound_re_ge_one
For re s ≥ 1, ‖Γ(s)‖ is bounded by a polynomial in ‖s‖.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:252
theorem
Complex.Gamma.stirling_bound_re_ge_zero
Main Stirling bound for Re(s) ≥ 0.
There exists a constant C such that for any s with re s ≥ 0 and
‖s‖ ≥ 1 we have ‖Γ(s)‖ ≤ exp (C · ‖s‖ · log (1 + ‖s‖)).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:348
theorem
Complex.Gamma.half_bound_re_ge_zero
Stirling bound specialized to Γ(s/2) for re s ≥ 0.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:521
lemma
Complex.Gammaℝ.Stirling.norm_cpow_pi_neg_half_le_one
The norm of π^{-s/2} is at most 1 when Re(s) ≥ 0.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:614
lemma
Complex.Gammaℝ.Stirling.norm_cpow_two_mul_pi_neg_le_one
The norm of (2π)^{-w} is at most 1 when Re(w) ≥ 0.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:627
theorem
Complex.Gammaℝ.Stirling.bound_re_ge_zero
Stirling bound for the archimedean factor Γ_ℝ = π^{-s/2} · Γ(s/2).
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:639
theorem
Complex.Gammaℝ.Stirling.finite_order
Finite order bound for Γ_ℝ.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:668
lemma
Complex.Gamma.norm_le_one_div_add_sqrt_pi_of_re_ge_of_re_le
If 0 < a ≤ re w ≤ 1, then ‖Γ(w)‖ ≤ 1 / a + √π.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/GammaBounds.lean:138
theorem
integral_interval_rpow_neg_one_sub
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean:23
theorem
integral_Ioi_rpow_neg_re_sub_one
∫_{1}^∞ u^{-re s - 1} = 1 / re s for 0 < re s.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean:58
lemma
Real.two_pow_floor_logb_le
The dyadic lower endpoint associated to ⌊log₂ x⌋ is at most x, for 1 ≤ x.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:28
lemma
Real.dyadicShell_lower_bound
If k = ⌊log₂ (x / r₀)⌋, then r₀ * 2^k is a lower dyadic bound for x.
PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:50
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.