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 781 to 800 of 1,644 declarations.
lemma
Ramanujan.integral_Icc_split
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:179
theorem
Ramanujan.low_contrib_le_three_tenths
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:223
theorem
Ramanujan.low_contrib_raw_le_three_tenths
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:292
lemma
Ramanujan.hasDerivAt_li_antideriv
The antiderivative x ↦ x / log x + ∫ 1 / log² u appearing in the integration-by-parts
identity for Li has derivative 1 / log t at any t > 1, provided the lower limit a of
the integral also exceeds 1 (so 1 / log² u is continuous across the interval).
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:334
lemma
Ramanujan.Li_eq_sub_add_integral
Integration by parts formula for Li(x).
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:354
theorem
Ramanujan.pi_error_identity
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:368
theorem
Ramanujan.integrable_theta
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:414
theorem
Ramanujan.pi_lower
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:471
theorem
Ramanujan.log_7_IBP
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:544
theorem
Ramanujan.log_8_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:595
theorem
Ramanujan.Calculations.a_exp_upper_of
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:689
theorem
Ramanujan.Calculations.B_le_small_of
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:721
theorem
Ramanujan.Calculations.C3_le_one_of
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:739
theorem
Ramanujan.Calculations.C1_le_one_of
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:767
lemma
RS_prime_helper.p_n_lower_small
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean:23
lemma
RS_prime_helper.pi_nth_prime'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean:57
lemma
RS_prime_helper.p_n_lower_large
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean:66
theorem
RS_prime.pntBigO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:22
theorem
RS_prime.pnt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:78
lemma
RS_prime.leftLim_theta_succ
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:139
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.