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 1 to 20 of 1,644 declarations.

lemma

HasDerivAt.of_hasDerivAt_ofReal_comp

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

PrimeNumberTheoremAnd.Auxiliary · PrimeNumberTheoremAnd/Auxiliary.lean:48

lemma

Backlund.zetaSurrogate_differentiable

The surrogate is entire: differentiable off 1 by congruence with (s - 1) · ζ(s), and at 1 by the removable-singularity criterion with the residue limit.

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:59

lemma

Backlund.zetaSurrogate_log_growth

The exponent-3/2 log-growth majorant for the surrogate. The exponent-1 form is FALSE on the left half-plane (|ζ(-2k-1)| ~ 2(2k+1)!/(2π)^{2k+2} via Bernoulli numbers: order 1 but maximal type), and x log x ≤ 2 x^(3/2) restores a true bound. Assembled from the three region lemmas above.

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:819

lemma

Backlund.zetaSurrogate_zeros_in_closedBall₀_count

Zero-mass-in-ball bound for the surrogate. An O(R) form would be false: the true mass in B(0, R) is ~ (R/2π) · log R (Riemann-von Mangoldt), which beats C' · (1 + R) for every fixed C'. The (1 + R)^(3/2) form follows directly from divisorMassClosedBall₀_le_of_growth at ρ = 3/2 plus the trailing-coefficient term (zetaSurrogate 0 = 1/2 ≠ 0, so that term is the constant |log (1/2)|).

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:856

lemma

Backlund.zeta_zero_re_mem_of_im_pos

Zeros of ζ with positive imaginary part lie in the closed strip 0 ≤ Re ≤ 1. Right edge: riemannZeta_ne_zero_of_one_le_re (mathlib) forces Re < 1. Left edge: for Re s < 0 the functional equation riemannZeta_one_sub writes ζ(s) as a nonvanishing prefactor times sin (π s / 2) · Γ(1 - s) · ζ(1 - s); the last two factors are nonzero (Re (1 - s) > 1), and Complex.sin_eq_zero_iff forces s real, contradicting 0 < Im s. Needed to place all counted zeros inside the single ball B(0, T + 1).

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:898

lemma

Backlund.zetaCounting_le_surrogate_mass

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

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:979

theorem

Backlund.zetaCounting_crude_majorant

A crude polynomial majorant for the zero-counting function riemannZeta.N, unconditional and with no argument-principle input. The constant is existential (the growth and ball-count inputs are existential); the intended consumer, dyadic summability over the zeta zeros, is indifferent to its value.

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:1101

lemma

AnalyticOn_divRemovable_zero

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

PrimeNumberTheoremAnd.BorelCaratheodory · PrimeNumberTheoremAnd/BorelCaratheodory.lean:41

lemma

AnalyticOn_divRemovable_zero_closedBall

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

PrimeNumberTheoremAnd.BorelCaratheodory · PrimeNumberTheoremAnd/BorelCaratheodory.lean:89

theorem

borelCaratheodory_closedBall

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

PrimeNumberTheoremAnd.BorelCaratheodory · PrimeNumberTheoremAnd/BorelCaratheodory.lean:220

theorem

BrunTitchmarsh.primesBetween_subset

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:61

theorem

BrunTitchmarsh.Ioc_filter_dvd_eq

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:101

theorem

BrunTitchmarsh.floor_div_approx

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:164

theorem

BrunTitchmarsh.abs_rem_le

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:181

theorem

BrunTitchmarsh.tmp

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:274

theorem

BrunTitchmarsh.prime_or_pow

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:354

theorem

BrunTitchmarsh.IsBigO.nat_Top_of_atTop

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

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:400

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.