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

theorem

Complex.analyticOrderAt_weierstrassFactor_div_self

The elementary factor z ↦ E_m (z / a) has a simple zero at a.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:152

lemma

Complex.weierstrassFactor_eq_exp_neg_tail

For ‖z‖ < 1 and z ≠ 1, E_m(z) = exp(-logTail_m(z)).

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:194

theorem

Complex.weierstrassFactor_sub_one_pow_bound

For ‖z‖ ≤ 1 / 2, ‖E_m(z) - 1‖ ≤ 4‖z‖^(m+1).

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:211

lemma

Complex.log_norm_weierstrassFactor_ge_log_norm_one_sub_sub

For ‖z‖ ≤ 1 / 2, ‖E_m(z) - 1‖ ≤ 4‖z‖^(m+1). -/ theorem weierstrassFactor_sub_one_pow_bound {m : ℕ} {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖weierstrassFactor m z - 1‖ ≤ 4 * ‖z‖ ^ (m + 1) := by by_cases hm : m = 0 · subst hm have hmain : ‖(1 - z) - 1‖ ≤ 4 * ‖z‖ ^ 1 := by have h : (1 - z) - 1 = -z := by ring calc ‖(1 - z) - 1‖ = ‖-z‖ := by simp [h] _ = ‖z‖ := norm_neg z _ = ‖z‖ ^ 1 := by simp _ ≤ 4 * ‖z‖ ^ 1 := by nlinarith [pow_nonneg (norm_nonneg z) 1] simpa [weierstrassFactor] using hmain · have hz_lt : ‖z‖ < 1 := lt_of_le_of_lt hz (by norm_num) by_cases hz1 : z = 1 · exfalso; rw [hz1] at hz; norm_num at hz have h_eq : weierstrassFactor m z = exp (-logTail m z) := weierstrassFactor_eq_exp_neg_tail m hz_lt hz1 rw [h_eq] have h_tail_bound := norm_logTail_le_two_mul_norm_pow hz_lt hz m have hw_le_one : ‖-logTail m z‖ ≤ 1 := by simp only [norm_neg] have : ‖logTail m z‖ ≤ 1 := by have hm_pos : 0 < m := Nat.pos_of_ne_zero hm have h2 : 2 ≤ m + 1 := by exact Nat.succ_le_succ (Nat.succ_le_iff.2 hm_pos) have hpow : (‖z‖ ^ (m + 1)) ≤ (‖z‖ ^ 2) := by have hz1' : ‖z‖ ≤ 1 := by nlinarith [hz] have hz0' : 0 ≤ ‖z‖ := norm_nonneg z exact pow_le_pow_of_le_one hz0' hz1' h2 have hmul : 2 * ‖z‖ ^ (m + 1) ≤ 2 * ‖z‖ ^ 2 := by gcongr have hsq : 2 * ‖z‖ ^ 2 ≤ 1 := by have hz0 : 0 ≤ ‖z‖ := norm_nonneg z have hz_sq : ‖z‖ ^ 2 ≤ (1 / 2 : ℝ) ^ 2 := pow_le_pow_left₀ hz0 hz 2 nlinarith exact (h_tail_bound.trans hmul).trans hsq linarith have h_exp_sub_one : ‖exp (-logTail m z) - 1‖ ≤ 2 * ‖-logTail m z‖ := Complex.norm_exp_sub_one_le hw_le_one simp only [norm_neg] at h_exp_sub_one calc ‖exp (-logTail m z) - 1‖ ≤ 2 * ‖logTail m z‖ := h_exp_sub_one _ ≤ 2 * (2 * ‖z‖ ^ (m + 1)) := by gcongr _ = 4 * ‖z‖ ^ (m + 1) := by ring

/-!

Lower bounds on Real.log ‖weierstrassFactor m z‖

Auxiliary inequalities for minimum-modulus / Cartan-type arguments in Hadamard factorization.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:261

lemma

Complex.log_norm_weierstrassFactor_ge_neg_two_pow

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:288

lemma

MeromorphicOn.divisor_support_inter_compact_finite

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport · PrimeNumberTheoremAnd/Mathlib/Analysis/Meromorphic/DivisorSupport.lean:64

lemma

Complex.logTaylor_succ_neg

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

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:59

lemma

Complex.hasDerivAt_partialLogSum

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

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:100

lemma

Complex.summable_logTail

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

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:135

lemma

Complex.norm_logTail_le

A coarse geometric-series bound for the logarithm tail. This intentionally drops the extra denominator m + 1 + k; the weaker estimate is the form used by the Weierstrass-factor bounds below.

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:161

lemma

Complex.norm_partialLogSum_le_nat_mul_max_one_norm_pow

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

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:208

lemma

Complex.neg_log_one_sub_eq_partialLogSum_add_logTail

Decompose the logarithm series into its first m terms and the remaining tail.

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:246

lemma

Real.mul_four_le_exp_add

Combine four elementary exponential majorants.

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Exp.lean:26

theorem

Complex.gamma_half_vertical_norm_sq

Exact critical-line identity: ‖Γ(1/2+iτ)‖² = π / cosh(πτ).

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.CriticalLineDecay · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/CriticalLineDecay.lean:38

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.