Skip to main content
therefore
Sign inSign up
Open navigation
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.

Research project325 GitHub starsApache-2.09 indexed versionsRepositoryFull history on Reservoir

Head version

a93551347dce

a93551347dce924b1db75d40218841bf085a465f

Toolchain
leanprover/lean4:v4.32.0
Revision date
22 Jul 2026
Dependencies
13
Versions
9

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

Package history

Showing 681 to 700 of 1,644 declarations.

lemma

Lcm.Criterion.val_two_M_ge_L'

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:465

lemma

Lcm.Criterion.val_p_M_ge_two

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:478

theorem

Lcm.Criterion.Ln_div_M_lt

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:590

theorem

Lcm.Criterion.not_highlyAbundant_1

\subsection{A sufficient condition}

We give a sufficient condition for σ(M)≥σ(Ln)\sigma(M) \geq \sigma(L_n).

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:664

theorem

Lcm.Criterion.not_highlyAbundant_2

Combining Lemma \ref{lem:criterion-sufficient} with Lemma \ref{lem:sigmaLn}, we see that it suffices to bound (\sigma(M)/M) from below in terms of (\sigma(L')/L'):

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:730

theorem

Lcm.exists_p_primes

To finish the proof we need to locate six primes p1,p2,p3,q1,q2,q3p_1,p_2,p_3,q_1,q_2,q_3 obeying the required inequality. Here we will rely on the prime number theorem of Dusart \cite{Dusart2018}.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1014

theorem

Lcm.exists_q_primes

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1071

theorem

Lcm.prod_q_ge

\subsection{Bounding the factors in \eqref{eq:main-ineq}}

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1224

theorem

Lcm.prod_p_ge

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1269

theorem

Lcm.pq_ratio_ge

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1332

theorem

Lcm.inv_n_pow_3_div_2_le

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:1427

theorem

Li2Bounds.log_one_minus_integrable

1/log(1-u) is integrable on [ε, 1) for ε > 0.

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:57

theorem

Li2Bounds.g_intervalIntegrable_full

g is integrable on [0, 1]. Uses boundedness by 2 from Li2Bounds.

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:86

theorem

Li2Bounds.pv_integral_eq_symmetric

The principal value integral for li(2) equals ∫_ε^1 g(u) du.

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:157

theorem

Li2Bounds.limit_integral_g

The limit as ε → 0⁺ of ∫_ε^1 g(u) du equals ∫_0^1 g(u) du.

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:169

theorem

Li2Bounds.setDiff_integral_eq_split

The Set.diff integral equals the split interval integrals.

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:199

theorem

LiSeries.integral_exp_sub_one_div_eq_tsum

The integral ∫₀ʸ (eᵘ - 1)/u du = ∑ y^(n+1) / ((n+1) · (n+1)!).

This is proved by integrating the power series (eᵘ-1)/u = ∑ uⁿ/(n+1)! term by term on [0, y]. Each term integrates to y^(n+1)/((n+1)(n+1)!).

PrimeNumberTheoremAnd.IEANTN.LiSeries · PrimeNumberTheoremAnd/IEANTN/LiSeries.lean:122

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.