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 versionsRepository Full 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 101 to 120 of 1,644 declarations.

theorem

BKLNW.prop_3

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:526

theorem

BKLNW.cor_3_1

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:567

theorem

BKLNW.prop_4_a

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:621

lemma

BKLNW.g_decreasing_interval

\subsection{Bounding theta(x)-x with a logarithmic decay, I: large x}

In this section and the next ones we obtain bounds of the shape $x \left(1 - \frac{m_k}{\log^k x}\right) \leq \theta(x)$ for all $x \geq X_0$ and $\theta(x) \leq x \left(1 + \frac{M_k}{\log^k x}\right)$ for all $x \geq X_1$ , for various $k, m_k, M_k, X_0, X_1$ , with $k \in \{1,\dots,5\}$ .

For this section we focus on estimates that are useful when $x$ is extremely large, e.g., $x \geq e^{25000}$ . -/

/- Show that the function g in the proof of the following lemma is decreasing

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:806

theorem

BKLNW.lem_6

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:832

theorem

BKLNW.bklnw_lemma_8

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1088

theorem

BKLNW.bklnw_eq_3_11

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1207

theorem

BKLNW.bklnw_cor_8_1a

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1275

theorem

BKLNW.bklnw_cor_8_1a_exact

Exact-B companion to bklnw_cor_8_1a: the same θ-bound stated with the Lemma-8 interval supremum B_8_exact instead of the looser Corollary-8.1 endpoint surrogate B_8_1. This is the intermediate already established inside bklnw_cor_8_1a (its h_main1, before the weakening B ≤ Btilde = B_8_1). It is what lets the retargeted bklnw_table_10_verification (B_8_exact ≤ listed value) chain into applications: |θ x - x| ≤ B_8_exact ≤ listed.

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1365

lemma

BKLNW.table_10_coverage

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1423

theorem

BKLNW.bklnw_cor_8_1b

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1447

theorem

BKLNW.bklnw_lemma_9

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1551

theorem

BKLNW.bklnw_table_from_buthe

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1634

theorem

BKLNW.bklnw_corollary_9_1

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1717

theorem

BKLNW.bklnw_table_12_verification

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1810

lemma

BKLNW.C_bk_le_Cb_of_M_eq_five_mul_ten_pow_ten

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1957

theorem

BKLNW.bklnw_corollary_9_1_explicit

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1975

theorem

BKLNW.thm_1b

See \cite[Table 15]{BKLNW} for values of $m_k$ and $M_k$ , for $k \in \{1,2,3,4,5\}$ . The first column of the table is the logarithmic threshold (b = \log X_0), so a row with first component (b) applies for (x \geq \exp b). -/) (latexEnv := "theorem")] theorem thm_1b_table {b : ℝ} (hb : b > 0) {M : Fin 5 → ℝ} (h : (b, M) ∈ Table_15) (k : Fin 5) {x : ℝ} (hx : x ≥ exp b) : x * (1 - M k / (log x)^(k.val + 1)) ≤ θ x ∧ θ x ≤ x * (1 + M k / (log x)^(k.val + 1)) := by sorry

/- [FIX]: This fixes a typo in the original paper https://arxiv.org/pdf/2002.11068.

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2189

theorem

cor_5_1_rem'

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean:599

theorem

BKLNW_app.bklnw_eq_A_9

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

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:86

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.