Adapted from PrimeNumberTheoremAnd revision 127b50e33f6033e2147921167a117af96d9ba4ea, via Jason Davies's Iwaniec linear sieve snapshot c8d01549d2ae640b36ec198c1f0f6495f1b036cf (both Apache-2.0). Blueprint-only machinery is omitted.

Supporting lemmas for Iwaniec's sieve and its prime-number-theorem input.

theorem AnalyticOn.norm_le_of_norm_le_on_sphere {C r R : ℝ} {f : ℂ → ℂ} {w : ℂ} (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ Metric.closedBall 0 r) : ‖f w‖ ≤ C

theorem IwaniecLinearSievePNT.borelCaratheodory' {M r R : ℝ} {f : ℂ → ℂ} {z : ℂ} (Mpos : 0 < M) (Rpos : 0 < R) (hyp_r : r < R) (analytic : AnalyticOn ℂ f (Metric.ball 0 R)) (zeroAtZero : f 0 = 0) (realPartBounded : ∀ z ∈ Metric.ball 0 R, (f z).re ≤ M) (hyp_z : z ∈ Metric.closedBall 0 r) : ‖f z‖ ≤ 2 * M * r / (R - r)

theorem IwaniecLinearSievePNT.cauchy_formula_deriv {r r' R : ℝ} {f : ℂ → ℂ} {z : ℂ} (r_lt_r' : r < r') (r'_lt_R : r' < R) (hf_on_ball : DifferentiableOn ℂ f (Metric.ball 0 R)) (hz : z ∈ Metric.closedBall 0 r) : deriv f z = (1 / (2 * ↑Real.pi * Complex.I)) • ∮ (w : ℂ) in C(0, r'), (w - z)⁻¹ ^ 2 • f w

theorem IwaniecLinearSievePNT.DerivativeBound {M r r' R : ℝ} {f : ℂ → ℂ} {z : ℂ} (Mpos : 0 < M) (pos_r : 0 < r) (r_lt_r' : r < r') (r'_lt_R : r' < R) (analytic_f : AnalyticOn ℂ f (Metric.ball 0 R)) (f_zero_at_zero : f 0 = 0) (re_f_le_M : ∀ z ∈ Metric.ball 0 R, (f z).re ≤ M) (z_in_r : z ∈ Metric.closedBall 0 r) : ‖deriv f z‖ ≤ 2 * M * r' ^ 2 / ((R - r') * (r' - r) ^ 2)

theorem IwaniecLinearSievePNT.BorelCaratheodoryDeriv {M r R : ℝ} {f : ℂ → ℂ} {z : ℂ} (Mpos : 0 < M) (rpos : 0 < r) (hyp_r : r < R) (analytic_f : AnalyticOn ℂ f (Metric.ball 0 R)) (zeroAtZero : f 0 = 0) (realPartBounded : ∀ z ∈ Metric.ball 0 R, (f z).re ≤ M) (hyp_z : z ∈ Metric.closedBall 0 r) : ‖deriv f z‖ ≤ 16 * M * R ^ 2 / (R - r) ^ 3

theorem IwaniecLinearSievePNT.LogOfAnalyticFunction {r R : ℝ} {B : ℂ → ℂ} (zero_lt_r : 0 < r) (r_lt_R : r < R) (BanalyticOnNhdOfDR : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (Bnonzero : ∀ z ∈ Metric.closedBall 0 R, B z ≠ 0) : ∃ (J_B : ℂ → ℂ), AnalyticOnNhd ℂ J_B (Metric.ball 0 R) ∧ J_B 0 = 0 ∧ (∀ z ∈ Metric.closedBall 0 r, deriv J_B z = deriv B z / B z) ∧ ∀ z ∈ Metric.ball 0 R, Real.log ‖B z‖ - Real.log ‖B 0‖ = (J_B z).re

theorem IwaniecLinearSievePNT.LogOfAnalyticFunction' {r' r R : ℝ} {B : ℂ → ℂ} (r'_pos : 0 < r') (r'_lt_r : r' < r) (r_lt_R : r < R) (BanalyticOnNhdOfDR : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (Bnonzero : ∀ z ∈ Metric.closedBall 0 r, B z ≠ 0) : ∃ (J_B : ℂ → ℂ), AnalyticOnNhd ℂ J_B (Metric.ball 0 r) ∧ J_B 0 = 0 ∧ (∀ z ∈ Metric.closedBall 0 r', deriv J_B z = deriv B z / B z) ∧ ∀ z ∈ Metric.ball 0 r, Real.log ‖B z‖ - Real.log ‖B 0‖ = (J_B z).re

def IwaniecLinearSievePNT.SetOfZeros (R : ℝ) (f : ℂ → ℂ) : Set ℂ

The zeros of f in the closed disk of radius R about the origin.

Equations

• IwaniecLinearSievePNT.SetOfZeros R f = {ρ : ℂ | ‖ρ‖ ≤ R ∧ f ρ = 0}

theorem IwaniecLinearSievePNT.finiteSetOfZeros_mono {r : ℝ} {f : ℂ → ℂ} (r_lt_one : r < 1) (finiteZeros : (SetOfZeros 1 f).Finite) : (SetOfZeros r f).Finite

noncomputable def IwaniecLinearSievePNT.ZeroFactor (f : ℂ → ℂ) (z : ℂ) : ℂ

The analytic factor remaining after removing the zero at z, evaluated at z.

Equations

• IwaniecLinearSievePNT.ZeroFactor f z = if h1 : AnalyticAt ℂ f z then if h2 : analyticOrderAt f z ≠ ⊤ then ⋯.choose z else 0 else 0

theorem IwaniecLinearSievePNT.ZeroFactorization {R : ℝ} {f : ℂ → ℂ} {ρ : ℂ} (RleOne : R < 1) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf_neq_zero_at_zero : f 0 ≠ 0) (hρ : ρ ∈ SetOfZeros R f) : ∃ (h_ρ : ℂ → ℂ), AnalyticAt ℂ h_ρ ρ ∧ h_ρ ρ ≠ 0 ∧ ZeroFactor f ρ = h_ρ ρ ∧ f =ᶠ[nhds ρ] fun (z : ℂ) => (z - ρ) ^ analyticOrderNatAt f ρ * h_ρ z

noncomputable def IwaniecLinearSievePNT.Cf (r : ℝ) (f : ℂ → ℂ) (z : ℂ) : ℂ

The analytic function obtained by removing the zeros of f in the disk of radius r.

Equations

• One or more equations did not get rendered due to their size.

theorem IwaniecLinearSievePNT.analyticAt_finset_prod_sub_pow (s : Finset ℂ) (g : ℂ → ℕ) (w : ℂ) : AnalyticAt ℂ (fun (z : ℂ) => ∏ ρ ∈ s, (z - ρ) ^ g ρ) w

theorem IwaniecLinearSievePNT.CfAnalytic {r R : ℝ} {f : ℂ → ℂ} (r_lt_R : r < R) (R_lt_one : R < 1) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf_neq_zero_at_zero : f 0 ≠ 0) : AnalyticOnNhd ℂ (Cf r f) (Metric.closedBall 0 R)

noncomputable def IwaniecLinearSievePNT.BlaschkeB (r R : ℝ) (f : ℂ → ℂ) (z : ℂ) : ℂ

The zero-removed function multiplied by the reflected zero factors at radius R.

Equations

• One or more equations did not get rendered due to their size.

theorem IwaniecLinearSievePNT.BlaschkeAnalytic {r R : ℝ} {f : ℂ → ℂ} (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1) (finiteZeros : (SetOfZeros 1 f).Finite) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf_neq_zero_at_zero : f 0 ≠ 0) : AnalyticOnNhd ℂ (BlaschkeB r R f) (Metric.closedBall 0 R)

theorem IwaniecLinearSievePNT.BlaschkeOfZero {r R : ℝ} {f : ℂ → ℂ} (r_pos : 0 < r) (r_lt_one : r < 1) (r_lt_R : r < R) (finiteZeros : (SetOfZeros 1 f).Finite) (hf_neq_zero_at_zero : f 0 ≠ 0) : ‖BlaschkeB r R f 0‖ = ‖f 0‖ * ∏ ρ ∈ ⋯.toFinset, (R / ‖ρ‖) ^ analyticOrderNatAt f ρ

theorem IwaniecLinearSievePNT.norm_fOfZero_le_norm_BlaschkeOfZero {r R : ℝ} {f : ℂ → ℂ} (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1) (finiteZeros : (SetOfZeros 1 f).Finite) (hf_neq_zero_at_zero : f 0 ≠ 0) : ‖f 0‖ ≤ ‖BlaschkeB r R f 0‖

theorem IwaniecLinearSievePNT.DiskBound {B r R : ℝ} {f : ℂ → ℂ} {z : ℂ} (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1) (finiteZeros : (SetOfZeros 1 f).Finite) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf_neq_zero_at_zero : f 0 ≠ 0) (fz_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (hz : z ∈ Metric.closedBall 0 R) : ‖BlaschkeB r R f z‖ ≤ B

theorem IwaniecLinearSievePNT.BlaschkeNonzero {r R : ℝ} {f : ℂ → ℂ} (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1) (finiteZeros : (SetOfZeros 1 f).Finite) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf_neq_zero_at_zero : f 0 ≠ 0) (z : ℂ) : z ∈ Metric.closedBall 0 r → BlaschkeB r R f z ≠ 0

theorem IwaniecLinearSievePNT.ZerosBound {B r R : ℝ} {f : ℂ → ℂ} (r_pos : 0 < r) (r_lt_one : r < 1) (r_lt_R : r < R) (R_lt_one : R < 1) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf0_eq_one : f 0 = 1) (finiteZeros : (SetOfZeros 1 f).Finite) (fz_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) : ↑(∑ ρ ∈ ⋯.toFinset, analyticOrderNatAt f ρ) ≤ 1 / Real.log (R / r) * Real.log B

noncomputable def IwaniecLinearSievePNT.JBlaschke {r' r R : ℝ} {f : ℂ → ℂ} (r'_pos : 0 < r') (r'_lt_r : r' < r) (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf0_eq_one : f 0 = 1) (finiteZeros : (SetOfZeros 1 f).Finite) (z : ℂ) : ℂ

An analytic logarithm of BlaschkeB on the smaller disk.

Equations

• IwaniecLinearSievePNT.JBlaschke r'_pos r'_lt_r r_pos r_lt_R R_lt_one hfAnalytic hf0_eq_one finiteZeros z = ⋯.choose z

theorem IwaniecLinearSievePNT.JBlaschkeDerivBound {B r' r R : ℝ} {f : ℂ → ℂ} {z : ℂ} (one_lt_B : 1 < B) (r'_pos : 0 < r') (r'_lt_r : r' < r) (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf0_eq_one : f 0 = 1) (finiteZeros : (SetOfZeros 1 f).Finite) (fz_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (hz : z ∈ Metric.closedBall 0 r') : ‖deriv (JBlaschke r'_pos r'_lt_r r_pos r_lt_R R_lt_one hfAnalytic hf0_eq_one finiteZeros) z‖ ≤ 16 * Real.log B * r ^ 2 / (r - r') ^ 3

theorem IwaniecLinearSievePNT.FinalBound {B r' r R' R : ℝ} {f : ℂ → ℂ} {z : ℂ} (one_lt_B : 1 < B) (r'_pos : 0 < r') (r'_lt_r : r' < r) (r_lt_one : r < 1) (r_lt_R' : r < R') (R'_lt_R : R' < R) (R_lt_one : R < 1) (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (hf0_eq_one : f 0 = 1) (finiteZeros : (SetOfZeros 1 f).Finite) (fz_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (hz : z ∈ Metric.closedBall 0 r' \ SetOfZeros R' f) : ‖deriv f z / f z - ∑ ρ ∈ ⋯.toFinset, ↑(analyticOrderNatAt f ρ) / (z - ρ)‖ ≤ (16 * r ^ 2 / (r - r') ^ 3 + 1 / ((R ^ 2 / R' - R') * Real.log (R / R'))) * Real.log B

theorem HasProd.nnnorm {α : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormMulClass R] [NormOneClass R] {f : α → R} {x : R} (hfx : HasProd f x) : HasProd (fun (x : α) => ‖f x‖₊) ‖x‖₊

theorem Multipliable.nnnorm {α : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormMulClass R] [NormOneClass R] {f : α → R} (hf : Multipliable f) : Multipliable fun (x : α) => ‖f x‖₊

theorem Multipliable.nnnorm_tprod {α : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormMulClass R] [NormOneClass R] {f : α → R} (hf : Multipliable f) : ‖∏' (i : α), f i‖₊ = ∏' (i : α), ‖f i‖₊

theorem IwaniecLinearSievePNT.ZetaFixedLowerBound (t : ℝ) : ‖riemannZeta (3 / 2 + Complex.I * ↑t)‖₊ ≥ ‖riemannZeta 3 / riemannZeta (3 / 2)‖₊

noncomputable def IwaniecLinearSievePNT.riemannZeta1 (s : ℂ) : ℂ

The integral continuation of zeta to positive real part, with its pole at 1 separated.

Equations

• IwaniecLinearSievePNT.riemannZeta1 s = 1 + 1 / (s - 1) - s * ∫ (u : ℝ) in Set.Ioi 1, ↑(Int.fract u) * ↑u ^ (-s - 1)

theorem IwaniecLinearSievePNT.Zeta1AltFormula {s : ℂ} (hs : 0 < s.re) : riemannZeta1 s = riemannZeta0 1 s

theorem IwaniecLinearSievePNT.ZetaAltFormula {s : ℂ} (hs : 0 < s.re) (hs' : s ≠ 1) : riemannZeta s = riemannZeta1 s

theorem IwaniecLinearSievePNT.GlobalBound {s : ℂ} (hs : ‖s‖ ≤ 1) {t : ℝ} (ht : |t| ≥ 2) : ‖riemannZeta (s + 3 / 2 + Complex.I * ↑t)‖ ≤ 7 + 2 * |t|

theorem IwaniecLinearSievePNT.norm_zeta_strict_mono_ofReal {a b : ℝ} (hb : 1 < b) (hab : b < a) : ‖riemannZeta ↑a‖ < ‖riemannZeta ↑b‖

theorem IwaniecLinearSievePNT.analyticOrderNatAt_fun_div_const {c z : ℂ} {f : ℂ → ℂ} (hc : c ≠ 0) (hfAnalytic : AnalyticAt ℂ f z) : analyticOrderNatAt (fun (z : ℂ) => f z / c) z = analyticOrderNatAt f z

theorem IwaniecLinearSievePNT.LogDerivZetaFinalBound {r' r R' R : ℝ} (r'_pos : 0 < r') (r'_lt_r : r' < r) (r_lt_one : r < 1) (r_lt_R' : r < R') (R'_lt_R : R' < R) (R_lt_one : R < 1) : ∃ C > 0, ∀ (t : ℝ), |t| ≥ 2 → let f := fun (z : ℂ) => riemannZeta (z + 3 / 2 + Complex.I * ↑t); ∀ (finiteZeros : (SetOfZeros 1 f).Finite), ∀ z ∈ Metric.closedBall 0 r' \ SetOfZeros R' f, ‖deriv f z / f z - ∑ ρ ∈ ⋯.toFinset, ↑(analyticOrderNatAt f ρ) / (z - ρ)‖ ≤ (16 * r ^ 2 / (r - r') ^ 3 + 1 / ((R ^ 2 / R' - R') * Real.log (R / R'))) * (C * Real.log |t|)

theorem IwaniecLinearSievePNT.ZetaShiftFiniteZeros {t : ℝ} (ht : |t| ≥ 2) {f : ℂ → ℂ} (hf : f = fun (z : ℂ) => riemannZeta (z + 3 / 2 + Complex.I * ↑t)) : (SetOfZeros 1 f).Finite

def IwaniecLinearSievePNT.ZeroWindow (t : ℝ) : Set ℂ

The zeros of zeta within distance 3 / 4 of 3 / 2 + I * t.

Equations

• IwaniecLinearSievePNT.ZeroWindow t = {ρ : ℂ | riemannZeta ρ = 0 ∧ ‖ρ - (3 / 2 + Complex.I * ↑t)‖ ≤ 3 / 4}

theorem IwaniecLinearSievePNT.analyticOrderNatAt_fun_comp_add_left (g : ℂ → ℂ) (c z : ℂ) : analyticOrderNatAt (fun (z : ℂ) => g (c + z)) z = analyticOrderNatAt g (c + z)

theorem IwaniecLinearSievePNT.analyticOrderNatAt_fun_comp_add_right (g : ℂ → ℂ) (c z : ℂ) : analyticOrderNatAt (fun (z : ℂ) => g (z + c)) z = analyticOrderNatAt g (z + c)

theorem IwaniecLinearSievePNT.SumBoundI : ∃ C > 0, ∀ δ ∈ Set.Ioo 0 1, ∀ (t : ℝ), |t| ≥ 2 → ∀ (finiteZeros : (ZeroWindow t).Finite), ‖deriv riemannZeta (1 + ↑δ + Complex.I * ↑t) / riemannZeta (1 + ↑δ + Complex.I * ↑t) - ∑ ρ ∈ finiteZeros.toFinset, ↑(analyticOrderNatAt riemannZeta ρ) / (1 + ↑δ + Complex.I * ↑t - ρ)‖ ≤ C * Real.log |t|

theorem IwaniecLinearSievePNT.ShiftTwoBound : ∃ C > 0, ∀ δ ∈ Set.Ioo 0 1, ∀ (t : ℝ), |t| ≥ 2 → (ZeroWindow (2 * t)).Finite → -(deriv riemannZeta (1 + ↑δ + 2 * Complex.I * ↑t) / riemannZeta (1 + ↑δ + 2 * Complex.I * ↑t)).re ≤ C * Real.log |t|

theorem IwaniecLinearSievePNT.ShiftOneBound : ∃ C > 0, ∀ δ ∈ Set.Ioo 0 1, ∀ (t : ℝ), |t| ≥ 2 → (ZeroWindow t).Finite → ∀ (ρ : ℂ), riemannZeta ρ = 0 → t = ρ.im → -(deriv riemannZeta (1 + ↑δ + Complex.I * ↑t) / riemannZeta (1 + ↑δ + Complex.I * ↑t)).re ≤ C * Real.log |t| - 1 / (1 + δ - ρ.re)

theorem IwaniecLinearSievePNT.ShiftZeroBound : ∃ C ≥ 1, ∀ δ ∈ Set.Ioo 0 1, -(deriv riemannZeta (1 + ↑δ) / riemannZeta (1 + ↑δ)).re ≤ 1 / δ + C

theorem IwaniecLinearSievePNT.vonMangoldtLSeriesSummable {s : ℂ} (hs : 1 < s.re) : Summable fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ s

theorem IwaniecLinearSievePNT.ZeroWindowFinite {t : ℝ} (ht : |t| ≥ 2) : (ZeroWindow t).Finite

theorem IwaniecLinearSievePNT.ZeroInequality : ∃ E ∈ Set.Ioo 0 (1 / 14), ∀ (ρ : ℂ), riemannZeta ρ = 0 → ∀ (σ : ℝ), σ = ρ.re → ∀ (t : ℝ), t = ρ.im → |t| ≥ 2 → σ ≤ 1 - E / Real.log |t|

noncomputable def IwaniecLinearSievePNT.E : ℝ

A positive constant in the zero-free-region inequality ZeroInequality.

Equations

• IwaniecLinearSievePNT.E = IwaniecLinearSievePNT.ZeroInequality.choose

theorem IwaniecLinearSievePNT.EinIoo : E ∈ Set.Ioo 0 (1 / 14)

theorem IwaniecLinearSievePNT.ZeroInequalitySpec (ρ : ℂ) : riemannZeta ρ = 0 → ∀ (σ : ℝ), σ = ρ.re → ∀ (t : ℝ), t = ρ.im → |t| ≥ 2 → σ ≤ 1 - E / Real.log |t|

noncomputable def IwaniecLinearSievePNT.DeltaT (t : ℝ) : ℝ

The width E / log |t| of the zero-free region at height t.

Equations

• IwaniecLinearSievePNT.DeltaT t = IwaniecLinearSievePNT.E / Real.log |t|

theorem IwaniecLinearSievePNT.DeltaRange (t : ℝ) : |t| ≥ 2 → DeltaT t < 1 / 9

theorem IwaniecLinearSievePNT.SumBoundII : ∃ C > 0, ∀ (t : ℝ), |t| ≥ 2 → ∀ (z : ℂ), t = z.im → z.re ∈ Set.Icc (1 - DeltaT t / 3) (3 / 2) → ∀ (finiteZeros : (ZeroWindow t).Finite), ‖deriv riemannZeta z / riemannZeta z - ∑ ρ ∈ finiteZeros.toFinset, ↑(analyticOrderNatAt riemannZeta ρ) / (z - ρ)‖ ≤ C * Real.log |t|

theorem IwaniecLinearSievePNT.GapSize (t : ℝ) (ht : |t| ≥ 3) (z : ℂ) (hzRe : z.re ∈ Set.Icc (1 - DeltaT t / 3) (3 / 2)) (ρ : ℂ) (hρ : ρ ∈ ZeroWindow t) : ‖z - ρ‖ ≥ DeltaT t / 6

theorem IwaniecLinearSievePNT.LogDerivZetaUniformLogSquaredBoundStrip : ∃ (F : ℝ) (_ : F = E / 3) (C : ℝ) (_ : 0 < C), ∀ (t : ℝ), 3 ≤ |t| → ∀ σ ∈ Set.Icc (1 - F / Real.log |t|) (3 / 2), ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 2

noncomputable def IwaniecLinearSievePNT.F : ℝ

The zero-free-strip constant used in the uniform log-squared bound.

Equations

• IwaniecLinearSievePNT.F = IwaniecLinearSievePNT.LogDerivZetaUniformLogSquaredBoundStrip.choose

theorem IwaniecLinearSievePNT.Fequ : F = E / 3

theorem IwaniecLinearSievePNT.FinIoo : F ∈ Set.Ioo 0 (1 / 42)

theorem IwaniecLinearSievePNT.LogDerivZetaUniformLogSquaredBoundStripSpec : ∃ (C : ℝ) (_ : 0 < C), ∀ (t : ℝ), 3 ≤ |t| → ∀ σ ∈ Set.Icc (1 - F / Real.log |t|) (3 / 2), ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 2

theorem IwaniecLinearSievePNT.FLogTtoDeltaT (t : ℝ) : DeltaT t / 3 = F / Real.log |t|

theorem IwaniecLinearSievePNT.LogDerivZetaBdd_of_Re_ge_three_halves : ∃ (C : ℝ), ∀ (s : ℂ), 3 / 2 ≤ s.re → ‖deriv riemannZeta s / riemannZeta s‖ ≤ C

theorem IwaniecLinearSievePNT.LogDerivZetaUniformLogSquaredBound : ∃ (C : ℝ) (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ici (1 - F / Real.log |t|) → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 2

theorem IwaniecLinearSievePNT.LogDerivZetaBndUnif12 : LogDerivZetaBndUnifGenProp 1 2

A wrapper for the above theorem

theorem IwaniecLinearSievePNT.ZetaZeroFree1 : ZetaZeroFreeGenProp 1

theorem IwaniecLinearSievePNT.LogDerivZetaHolcLargeT1 : LogDerivZetaHolcLargeTGenProp 1

theorem IwaniecLinearSievePNT.LogDerivZetaBoundedAndHolo12 : LogDerivZetaBoundedAndHoloGenProp 1 2

theorem IwaniecLinearSievePNT.StrongPNT : ∃ c > 0, (ChebyshevPsi - id) =O[Filter.atTop] fun (x : ℝ) => x * Real.exp (-c * Real.log x ^ (1 / 2))