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 741 to 760 of 1,644 declarations.
theorem
MobiusLemma.mobius_lemma_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.MobiusLemma · PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean:491
lemma
integral_exp_div_neg_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:32
lemma
integral_exp_div_split
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:46
lemma
integrableOn_one_sub_exp_neg_div
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:60
lemma
integrableOn_exp_neg_div_Ioi
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:73
lemma
integrableOn_exp_sub_one_div
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:87
lemma
tendsto_integral_one_sub_exp_neg_div
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:101
lemma
tendsto_integral_exp_neg_div_Ioi
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:122
lemma
tendsto_integral_exp_sub_one_div
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:136
lemma
pv_rewrite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:403
theorem
pv_exp_div_eq_gamma_add_log_add_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:437
lemma
HasPrimeInInterval.iff_pi_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:13
theorem
theta_pos_implies_prime_in_interval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:58
lemma
HasPrimeInInterval.iff_theta_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:72
lemma
Eθ.hasPrimeInInterval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:128
lemma
Eθ.numericalBound.hasPrimeInInterval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:161
lemma
Eθ.classicalBound.hasPrimeInInterval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:184
lemma
prime_gap_record.hasPrimeInInterval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:205
theorem
Ramanujan.sq_pi_lt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:28
theorem
Ramanujan.ex_pi_gt_neg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:148
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.