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 761 to 780 of 1,644 declarations.
theorem
Ramanujan.ex_pi_gt_nonneg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:281
theorem
Ramanujan.criterion
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:434
theorem
Ramanujan.pi_bound_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:507
theorem
Ramanujan.pi_bound_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:557
theorem
Ramanujan.pi_bound_3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:692
theorem
Ramanujan.pi_bound_4
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:805
theorem
Ramanujan.pi_bound_5
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:827
theorem
Ramanujan.pi_bound_6
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:843
theorem
Ramanujan.pi_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:868
theorem
Ramanujan.a_mono
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:931
lemma
Ramanujan.log_6_IBP_t
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1191
lemma
Ramanujan.log_5_IBP_t
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1242
lemma
Ramanujan.log_4_IBP_t
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1293
lemma
Ramanujan.log_3_IBP_t
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1344
lemma
Ramanujan.log_2_IBP_t
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1395
lemma
Ramanujan.log_2_expansion_t
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1446
theorem
Ramanujan.pi_upper_specific
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1740
theorem
Ramanujan.pi_lower_specific
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:2254
theorem
Ramanujan.epsilon_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:2406
theorem
Ramanujan.style_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:26
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.