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 Chebyshev.psi_eq_sum_range (x : ℝ) : psi x = ∑ n ∈ Finset.range (⌊x⌋₊ + 1), ArithmeticFunction.vonMangoldt n

@[reducible, inline]

noncomputable abbrev IwaniecLinearSievePNT.ChebyshevPsi (x : ℝ) : ℝ

The Chebyshev psi function used in the contour estimates.

Equations

• IwaniecLinearSievePNT.ChebyshevPsi x = Chebyshev.psi x

theorem IwaniecLinearSievePNT.LogDerivativeDirichlet (s : ℂ) (hs : 1 < s.re) : -deriv riemannZeta s / riemannZeta s = ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ s

@[reducible, inline]

noncomputable abbrev IwaniecLinearSievePNT.SmoothedChebyshevIntegrand (SmoothingF : ℝ → ℝ) (ε X : ℝ) : ℂ → ℂ

The Mellin integrand for the smoothed Chebyshev function.

Equations

• IwaniecLinearSievePNT.SmoothedChebyshevIntegrand SmoothingF ε X s = -deriv riemannZeta s / riemannZeta s * mellin (fun (x : ℝ) => ↑(IwaniecLinearSievePNT.Smooth1 SmoothingF ε x)) s * ↑X ^ s

noncomputable def IwaniecLinearSievePNT.SmoothedChebyshev (SmoothingF : ℝ → ℝ) (ε X : ℝ) : ℂ

The smoothed Chebyshev function, expressed by Mellin inversion.

Equations

• IwaniecLinearSievePNT.SmoothedChebyshev SmoothingF ε X = IwaniecLinearSievePNT.VerticalIntegral' (IwaniecLinearSievePNT.SmoothedChebyshevIntegrand SmoothingF ε X) (1 + (Real.log X)⁻¹)

theorem IwaniecLinearSievePNT.smoothedChebyshevIntegrand_conj {SmoothingF : ℝ → ℝ} {ε X : ℝ} (Xpos : 0 < X) (s : ℂ) : SmoothedChebyshevIntegrand SmoothingF ε X ((starRingEnd ℂ) s) = (starRingEnd ℂ) (SmoothedChebyshevIntegrand SmoothingF ε X s)

theorem IwaniecLinearSievePNT.SmoothedChebyshevDirichlet_aux_integrable {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ x > 0, 0 ≤ SmoothingF x) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) {σ : ℝ} (σ_gt : 1 < σ) (σ_le : σ ≤ 2) : MeasureTheory.Integrable (fun (y : ℝ) => mellin (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (↑σ + ↑y * Complex.I)) MeasureTheory.volume

theorem IwaniecLinearSievePNT.SmoothedChebyshevDirichlet_aux_tsum_integral {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ x > 0, 0 ≤ SmoothingF x) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) {X : ℝ} (X_pos : 0 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) {σ : ℝ} (σ_gt : 1 < σ) (σ_le : σ ≤ 2) : ∫ (t : ℝ), ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ (↑σ + ↑t * Complex.I) * mellin (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (↑σ + ↑t * Complex.I) * ↑X ^ (↑σ + ↑t * Complex.I) = ∑' (n : ℕ), ∫ (t : ℝ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ (↑σ + ↑t * Complex.I) * mellin (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (↑σ + ↑t * Complex.I) * ↑X ^ (↑σ + ↑t * Complex.I)

theorem IwaniecLinearSievePNT.SmoothedChebyshevDirichlet {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ x > 0, 0 ≤ SmoothingF x) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) {X : ℝ} (X_gt : 3 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) : SmoothedChebyshev SmoothingF ε X = ↑(∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * Smooth1 SmoothingF ε (↑n / X))

theorem IwaniecLinearSievePNT.SmoothedChebyshevClose_aux {Smooth1 : (ℝ → ℝ) → ℝ → ℝ → ℝ} (SmoothingF : ℝ → ℝ) (c₁ : ℝ) (c₁_pos : 0 < c₁) (c₁_lt : c₁ < 1) (c₂ : ℝ) (c₂_pos : 0 < c₂) (c₂_lt : c₂ < 2) (hc₂ : ∀ (ε x : ℝ), ε ∈ Set.Ioo 0 1 → 1 + c₂ * ε ≤ x → Smooth1 SmoothingF ε x = 0) (C : ℝ) (C_eq : C = 6 * (3 * c₁ + c₂)) (ε : ℝ) (ε_pos : 0 < ε) (ε_lt_one : ε < 1) (X : ℝ) (X_pos : 0 < X) (X_gt_three : 3 < X) (X_bound_1 : 1 ≤ X * ε * c₁) (X_bound_2 : 1 ≤ X * ε * c₂) (smooth1BddAbove : ∀ (n : ℕ), 0 < n → Smooth1 SmoothingF ε (↑n / X) ≤ 1) (smooth1BddBelow : ∀ (n : ℕ), 0 < n → Smooth1 SmoothingF ε (↑n / X) ≥ 0) (smoothIs1 : ∀ (n : ℕ), 0 < n → ↑n ≤ X * (1 - c₁ * ε) → Smooth1 SmoothingF ε (↑n / X) = 1) (smoothIs0 : ∀ (n : ℕ), 1 + c₂ * ε ≤ ↑n / X → Smooth1 SmoothingF ε (↑n / X) = 0) : ‖↑(∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * Smooth1 SmoothingF ε (↑n / X)) - ↑(Chebyshev.psi X)‖ ≤ C * ε * X * Real.log X

theorem IwaniecLinearSievePNT.SmoothedChebyshevClose {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) : ∃ C > 0, ∀ (X : ℝ), 3 < X → ∀ (ε : ℝ), 0 < ε → ε < 1 → 2 < X * ε → ‖SmoothedChebyshev SmoothingF ε X - ↑(Chebyshev.psi X)‖ ≤ C * ε * X * Real.log X

def IwaniecLinearSievePNT.LogDerivZetaHasBound (n₁ n₂ A C : ℝ) : Prop

A uniform logarithmic bound for the logarithmic derivative of zeta near the line re = 1.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₁ (SmoothingF : ℝ → ℝ) (ε X T : ℝ) : ℂ

The lower infinite vertical tail of the normalized Perron contour.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₂ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ

The lower horizontal segment at imaginary part -T.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₃₇ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ

The central vertical contour before splitting at imaginary parts -3 and 3.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₈ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ

The upper horizontal segment at imaginary part T.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₉ (SmoothingF : ℝ → ℝ) (ε X T : ℝ) : ℂ

The upper infinite vertical tail of the normalized Perron contour.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₃ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ

The lower vertical segment from imaginary part -T to -3.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₇ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ

The upper vertical segment from imaginary part 3 to T.

Equations

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

noncomputable def IwaniecLinearSievePNT.I₄ (SmoothingF : ℝ → ℝ) (ε X σ₁ σ₂ : ℝ) : ℂ

The lower horizontal segment at imaginary part -3.

Equations

• IwaniecLinearSievePNT.I₄ SmoothingF ε X σ₁ σ₂ = 1 / (2 * ↑Real.pi * Complex.I) * ∫ (σ : ℝ) in σ₂..σ₁, IwaniecLinearSievePNT.SmoothedChebyshevIntegrand SmoothingF ε X (↑σ - 3 * Complex.I)

noncomputable def IwaniecLinearSievePNT.I₆ (SmoothingF : ℝ → ℝ) (ε X σ₁ σ₂ : ℝ) : ℂ

The upper horizontal segment at imaginary part 3.

Equations

• IwaniecLinearSievePNT.I₆ SmoothingF ε X σ₁ σ₂ = 1 / (2 * ↑Real.pi * Complex.I) * ∫ (σ : ℝ) in σ₂..σ₁, IwaniecLinearSievePNT.SmoothedChebyshevIntegrand SmoothingF ε X (↑σ + 3 * Complex.I)

noncomputable def IwaniecLinearSievePNT.I₅ (SmoothingF : ℝ → ℝ) (ε X σ₂ : ℝ) : ℂ

The central vertical segment between imaginary parts -3 and 3.

Equations

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

theorem IwaniecLinearSievePNT.realDiff_of_complexDiff {f : ℂ → ℂ} (s : ℂ) (hf : DifferentiableAt ℂ f s) : ContinuousAt (fun (x : ℝ) => f (↑s.re + ↑x * Complex.I)) s.im

def IwaniecLinearSievePNT.LogDerivZetaIsHoloSmall (σ₂ : ℝ) : Prop

Holomorphy of the logarithmic derivative on the small rectangle, away from its pole.

Equations

• IwaniecLinearSievePNT.LogDerivZetaIsHoloSmall σ₂ = IwaniecLinearSievePNT.HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.uIcc σ₂ 2 ×ℂ Set.uIcc (-3) 3 \ {1})

theorem IwaniecLinearSievePNT.dlog_riemannZeta_bdd_on_vertical_lines_explicit {σ₀ : ℝ} (σ₀_gt : 1 < σ₀) (t : ℝ) : ‖-deriv riemannZeta (↑σ₀ + ↑t * Complex.I) / riemannZeta (↑σ₀ + ↑t * Complex.I)‖ ≤ ‖deriv riemannZeta ↑σ₀ / riemannZeta ↑σ₀‖

theorem IwaniecLinearSievePNT.dlog_riemannZeta_bdd_on_vertical_lines {σ₀ : ℝ} (σ₀_gt : 1 < σ₀) : ∃ c > 0, ∀ (t : ℝ), ‖deriv riemannZeta (↑σ₀ + ↑t * Complex.I) / riemannZeta (↑σ₀ + ↑t * Complex.I)‖ ≤ c

theorem IwaniecLinearSievePNT.SmoothedChebyshevPull1_aux_integrable {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (ε_lt_one : ε < 1) {X : ℝ} (X_gt : 3 < X) {σ₀ : ℝ} (σ₀_gt : 1 < σ₀) (σ₀_le_2 : σ₀ ≤ 2) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) : MeasureTheory.Integrable (fun (t : ℝ) => SmoothedChebyshevIntegrand SmoothingF ε X (↑σ₀ + ↑t * Complex.I)) MeasureTheory.volume

theorem IwaniecLinearSievePNT.BddAboveOnRect {g : ℂ → ℂ} {z w : ℂ} (holoOn : HolomorphicOn g (z.Rectangle w)) : BddAbove (norm ∘ g '' z.Rectangle w)

theorem IwaniecLinearSievePNT.SmoothedChebyshevPull1 {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (ε_lt_one : ε < 1) (X : ℝ) (X_gt : 3 < X) {T : ℝ} (T_pos : 0 < T) {σ₁ : ℝ} (σ₁_pos : 0 < σ₁) (σ₁_lt_one : σ₁ < 1) (holoOn : HolomorphicOn (deriv riemannZeta / riemannZeta) (Set.Icc σ₁ 2 ×ℂ Set.Icc (-T) T \ {1})) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) : SmoothedChebyshev SmoothingF ε X = I₁ SmoothingF ε X T - I₂ SmoothingF ε T X σ₁ + I₃₇ SmoothingF ε T X σ₁ + I₈ SmoothingF ε T X σ₁ + I₉ SmoothingF ε X T + mellin (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) 1 * ↑X

theorem IwaniecLinearSievePNT.interval_membership (r a b : ℝ) (h1 : r ∈ Set.Icc (min a b) (max a b)) (h2 : a < b) : a ≤ r ∧ r ≤ b

theorem IwaniecLinearSievePNT.verticalIntegral_split_three_finite {s a b e σ : ℝ} {f : ℂ → ℂ} (hf : MeasureTheory.IntegrableOn (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) (Set.Icc s e) MeasureTheory.volume) (hab : s < a ∧ a < b ∧ b < e) : VIntegral f σ s e = VIntegral f σ s a + VIntegral f σ a b + VIntegral f σ b e

theorem IwaniecLinearSievePNT.verticalIntegral_split_three_finite' {s a b e σ : ℝ} {f : ℂ → ℂ} (hf : MeasureTheory.IntegrableOn (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) (Set.Icc s e) MeasureTheory.volume) (hab : s < a ∧ a < b ∧ b < e) : 1 / (2 * ↑Real.pi * Complex.I) * VIntegral f σ s e = 1 / (2 * ↑Real.pi * Complex.I) * VIntegral f σ s a + 1 / (2 * ↑Real.pi * Complex.I) * VIntegral f σ a b + 1 / (2 * ↑Real.pi * Complex.I) * VIntegral f σ b e

theorem IwaniecLinearSievePNT.SmoothedChebyshevPull2_aux1 {T σ₁ : ℝ} (σ₁lt : σ₁ < 1) (holoOn : HolomorphicOn (deriv riemannZeta / riemannZeta) (Set.Icc σ₁ 2 ×ℂ Set.Icc (-T) T \ {1})) : ContinuousOn (fun (t : ℝ) => -deriv riemannZeta (↑σ₁ + ↑t * Complex.I) / riemannZeta (↑σ₁ + ↑t * Complex.I)) (Set.Icc (-T) T)

theorem IwaniecLinearSievePNT.SmoothedChebyshevPull2 {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (ε_lt_one : ε < 1) (X : ℝ) : 3 < X → ∀ {T : ℝ} (T_pos : 3 < T) {σ₁ σ₂ : ℝ} (σ₂_pos : 0 < σ₂) (σ₁_lt_one : σ₁ < 1) (σ₂_lt_σ₁ : σ₂ < σ₁) (holoOn : HolomorphicOn (deriv riemannZeta / riemannZeta) (Set.Icc σ₁ 2 ×ℂ Set.Icc (-T) T \ {1})) (holoOn2 : HolomorphicOn (SmoothedChebyshevIntegrand SmoothingF ε X) (Set.Icc σ₂ 2 ×ℂ Set.Icc (-3) 3 \ {1})) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) (diff_SmoothingF : ContDiff ℝ 1 SmoothingF), I₃₇ SmoothingF ε T X σ₁ = I₃ SmoothingF ε T X σ₁ - I₄ SmoothingF ε X σ₁ σ₂ + I₅ SmoothingF ε X σ₂ + I₆ SmoothingF ε X σ₁ σ₂ + I₇ SmoothingF ε T X σ₁

theorem IwaniecLinearSievePNT.ZetaBoxEval {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) : ∃ (C : ℝ), ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (X : ℝ), 0 ≤ X → ‖mellin (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) 1 * ↑X - ↑X‖ ≤ C * ε * X

theorem IwaniecLinearSievePNT.poisson_kernel_integrable (x : ℝ) (hx : x ≠ 0) : MeasureTheory.Integrable (fun (t : ℝ) => (‖↑x + ↑t * Complex.I‖ ^ 2)⁻¹) MeasureTheory.volume

theorem IwaniecLinearSievePNT.ae_volume_of_contains_compl_singleton_zero (s : Set ℝ) (h : Set.univ \ {0} ⊆ s) : s ∈ MeasureTheory.ae MeasureTheory.volume

theorem IwaniecLinearSievePNT.integral_evaluation (x T : ℝ) (T_large : 3 < T) : ∫ (t : ℝ) in Set.Iic (-T), (‖↑x + ↑t * Complex.I‖ ^ 2)⁻¹ ≤ T⁻¹

theorem IwaniecLinearSievePNT.IBound_aux1 (X₀ : ℝ) (X₀pos : X₀ > 0) {k : ℝ} (k_pos : 0 < k) : ∃ C ≥ 1, ∀ X ≥ X₀, Real.log X ^ k ≤ C * X

def IwaniecLinearSievePNT.I1BoundGenProp (SmoothingF : ℝ → ℝ) : Prop

The uniform estimate for contour segment I₁ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I1Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) : I1BoundGenProp SmoothingF

theorem IwaniecLinearSievePNT.I9I1 {SmoothingF : ℝ → ℝ} {ε X T : ℝ} (Xpos : 0 < X) : I₉ SmoothingF ε X T = (starRingEnd ℂ) (I₁ SmoothingF ε X T)

def IwaniecLinearSievePNT.I9BoundGenProp (SmoothingF : ℝ → ℝ) : Prop

The uniform estimate for contour segment I₉ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I9Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) : I9BoundGenProp SmoothingF

theorem IwaniecLinearSievePNT.one_add_inv_log {X : ℝ} (X_ge : 3 ≤ X) : 1 + (Real.log X)⁻¹ < 2

def IwaniecLinearSievePNT.I2BoundGenProp (n : ℝ) (SmoothingF : ℝ → ℝ) (A : ℝ) : Prop

The uniform estimate for contour segment I₂ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I2GenBound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {n₁ n₂ : ℝ} (n₁_pos : 0 < n₁) (n₂_pos : 0 < n₂) {A C₂ : ℝ} (has_bound : LogDerivZetaHasBound n₁ n₂ A C₂) (C₂pos : 0 < C₂) (A_in : A ∈ Set.Ioc 0 (1 / 2)) : I2BoundGenProp n₁ SmoothingF A

theorem IwaniecLinearSievePNT.I8I2 {SmoothingF : ℝ → ℝ} {X ε T σ₁ : ℝ} (T_gt : 3 < T) : I₈ SmoothingF ε X T σ₁ = -(starRingEnd ℂ) (I₂ SmoothingF ε X T σ₁)

def IwaniecLinearSievePNT.I8BoundGenProp (n : ℝ) (SmoothingF : ℝ → ℝ) (A : ℝ) : Prop

The uniform estimate for contour segment I₈ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I8GenBound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {n₁ n₂ : ℝ} (n₁_pos : 0 < n₁) (n₂_pos : 0 < n₂) {A C₂ : ℝ} (has_bound : LogDerivZetaHasBound n₁ n₂ A C₂) (C₂_pos : 0 < C₂) (A_in : A ∈ Set.Ioc 0 (1 / 2)) : I8BoundGenProp n₁ SmoothingF A

theorem Real.log_le_const_mul_rpow {c x : ℝ} (hc : 0 < c) (hx : 0 < x) : log x ≤ c * x ^ (1 / c)

theorem IwaniecLinearSievePNT.log_pow_over_xsq_integral_bounded (n : ℝ) (n_pos : 0 < n) : ∃ (C : ℝ), 0 < C ∧ ∀ T > 3, ∫ (x : ℝ) in Set.Ioo 3 T, Real.log x ^ n / x ^ 2 < C

def IwaniecLinearSievePNT.I3BoundGenProp (n : ℝ) (SmoothingF : ℝ → ℝ) (A : ℝ) : Prop

The uniform estimate for contour segment I₃ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I3GenBound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {n₁ n₂ : ℝ} (n₁_pos : 0 < n₁) (n₂_pos : 0 < n₂) {A Cζ : ℝ} (hCζ : LogDerivZetaHasBound n₁ n₂ A Cζ) (Cζpos : 0 < Cζ) (hA : A ∈ Set.Ioc 0 (1 / 2)) : I3BoundGenProp n₁ SmoothingF A

theorem IwaniecLinearSievePNT.I7I3 {SmoothingF : ℝ → ℝ} {ε X T σ₁ : ℝ} (Xpos : 0 < X) : I₇ SmoothingF ε T X σ₁ = (starRingEnd ℂ) (I₃ SmoothingF ε T X σ₁)

def IwaniecLinearSievePNT.I7BoundGenProp (n : ℝ) (SmoothingF : ℝ → ℝ) (A : ℝ) : Prop

The uniform estimate for contour segment I₇ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I7GenBound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {n₁ n₂ : ℝ} (n₁_pos : 0 < n₁) (n₂_pos : 0 < n₂) {A Cζ : ℝ} (hCζ : LogDerivZetaHasBound n₁ n₂ A Cζ) (Cζpos : 0 < Cζ) (hA : A ∈ Set.Ioc 0 (1 / 2)) : I7BoundGenProp n₁ SmoothingF A

def IwaniecLinearSievePNT.I4BoundGenProp (n : ℝ) (SmoothingF : ℝ → ℝ) (A σ₂ : ℝ) : Prop

The uniform estimate for contour segment I₄ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I4GenBound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Set.Ioo 0 1) {n : ℝ} (n_pos : n > 0) {A : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) : I4BoundGenProp n SmoothingF A σ₂

theorem IwaniecLinearSievePNT.I6I4 {SmoothingF : ℝ → ℝ} {ε X σ₁ σ₂ : ℝ} (Xpos : 0 < X) : I₆ SmoothingF ε X σ₁ σ₂ = -(starRingEnd ℂ) (I₄ SmoothingF ε X σ₁ σ₂)

def IwaniecLinearSievePNT.I6BoundGenProp (n : ℝ) (SmoothingF : ℝ → ℝ) (A σ₂ : ℝ) : Prop

The uniform estimate for contour segment I₆ used in the PNT argument.

Equations

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

theorem IwaniecLinearSievePNT.I6GenBound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Set.Ioo 0 1) {n : ℝ} (n_pos : 0 < n) {A : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) : I6BoundGenProp n SmoothingF A σ₂

def IwaniecLinearSievePNT.I5BoundGenProp (SmoothingF : ℝ → ℝ) (σ₂ : ℝ) : Prop

The uniform estimate for contour segment I₅ used in the PNT argument.

Equations

• IwaniecLinearSievePNT.I5BoundGenProp SmoothingF σ₂ = ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ‖IwaniecLinearSievePNT.I₅ SmoothingF ε X σ₂‖ ≤ C * X ^ σ₂ / ε

theorem IwaniecLinearSievePNT.I5Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Set.Ioo 0 1) : I5BoundGenProp SmoothingF σ₂

def IwaniecLinearSievePNT.LogDerivZetaBoundedAndHoloGenProp (n₁ n₂ : ℝ) : Prop

A zero-free rectangle with a uniform bound for the logarithmic derivative of zeta.

Equations

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

theorem IwaniecLinearSievePNT.LogDerivZetaBoundedAndHoloGen {n₁ n₂ : ℝ} (LogDerivZetaBndUnif : LogDerivZetaBndUnifGenProp n₁ n₂) (LogDerivZetaHolcLargeT : LogDerivZetaHolcLargeTGenProp n₁) : LogDerivZetaBoundedAndHoloGenProp n₁ n₂

theorem IwaniecLinearSievePNT.LogDerivZetaBoundedAndHolo99 : LogDerivZetaBoundedAndHoloGenProp 9 9

theorem IwaniecLinearSievePNT.MellinOfSmooth1cExplicit {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : ∃ (ε₀ : ℝ) (c : ℝ), 0 < ε₀ ∧ 0 < c ∧ ∀ ε ∈ Set.Ioo 0 ε₀, ‖mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) 1 - 1‖ ≤ c * ε

theorem IwaniecLinearSievePNT.x_ε_to_inf (c : ℝ) {B : ℝ} (B_le : B < 1) : Filter.Tendsto (fun (x : ℝ) => x * Real.exp (-c * Real.log x ^ B)) Filter.atTop Filter.atTop

theorem IwaniecLinearSievePNT.GenStrengthPNT {n₁ n₂ : ℝ} (LogDerivZetaBoundedAndHolo : LogDerivZetaBoundedAndHoloGenProp n₁ n₂) (n₁_pos : 0 < n₁) (n₂_pos : 0 < n₂) : ∃ c > 0, (Chebyshev.psi - id) =O[Filter.atTop] fun (x : ℝ) => x * Real.exp (-c * Real.log x ^ (1 / (1 + n₁)))

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

*** Prime Number Theorem (Medium Strength) *** The ChebyshevPsi function is asymptotic to x.