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 81 to 100 of 1,644 declarations.
lemma
euler_maclaurin_tendsto
γ₂ converges to γ.
PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:199
lemma
γ₃_increasing
γ₃ is strictly increasing for n ≥ 1.
PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:433
lemma
γ₃_lower_bound
γ₃ n < γ for all n ≥ 1.
PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:471
theorem
fourierIntegral_self_add_deriv_deriv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:59
lemma
tendsto_const_mul_log_add_two_div_add_two_atTop
The decay K * (log (T + 2) / (T + 2)) → 0 as T → ∞, for any constant K.
PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:85
lemma
norm_fourier_le_integral_deriv_div
Fourier-transform decay from an integrable derivative: for integrable,
differentiable g with integrable derivative, ‖𝓕 g w‖ ≤ (∫ ‖deriv g x‖) / (2π·|w|).
PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:98
lemma
norm_oscillatory_integral_le_integral_deriv_div
The oscillatory-integral form of the decay bound: for 0 < T,
‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / T.
PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:127
lemma
norm_oscillatory_integral_le_integral_deriv_div_abs
The |T| variant of the oscillatory-integral decay bound: for T ≠ 0,
‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / |T|.
PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:159
theorem
BKLNW.buthe_eq_1_7
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:40
theorem
BKLNW.lemma_11a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:74
theorem
BKLNW.lemma_11b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:87
theorem
BKLNW.thm_1a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:127
theorem
BKLNW.thm_1a_crit
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:160
theorem
BKLNW.cor_2_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:184
theorem
BKLNW.prop_3_sub_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:238
theorem
BKLNW.prop_3_sub_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:296
theorem
BKLNW.prop_3_sub_3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:326
lemma
BKLNW.sum_gt.aux
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:356
theorem
BKLNW.prop_3_sub_6
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:437
theorem
BKLNW.prop_3_sub_7
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:478
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.