theorem Chebyshev.psi_eq_sum_range (x : ℝ) : psi x = ∑ n ∈ Finset.range (⌊x⌋₊ + 1), ArithmeticFunction.vonMangoldt n

@[reducible, inline]

noncomputable abbrev ChebyshevPsi (x : ℝ) : ℝ

Equations

• ChebyshevPsi x = Chebyshev.psi x

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

theorem 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 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 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 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 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

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

Equations

• I₁ SmoothingF ε X T = 1 / (2 * ↑Real.pi * Complex.I) * (Complex.I * ∫ (t : ℝ) in Set.Iic (-T), SmoothedChebyshevIntegrand SmoothingF ε X (1 + ↑(Real.log X)⁻¹ + ↑t * Complex.I))

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

Equations

• I₂ SmoothingF ε T X σ₁ = 1 / (2 * ↑Real.pi * Complex.I) * ∫ (σ : ℝ) in σ₁..1 + (Real.log X)⁻¹, SmoothedChebyshevIntegrand SmoothingF ε X (↑σ - ↑T * Complex.I)

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

Equations

• I₃₇ SmoothingF ε T X σ₁ = 1 / (2 * ↑Real.pi * Complex.I) * (Complex.I * ∫ (t : ℝ) in -T..T, SmoothedChebyshevIntegrand SmoothingF ε X (↑σ₁ + ↑t * Complex.I))

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

Equations

• I₈ SmoothingF ε T X σ₁ = 1 / (2 * ↑Real.pi * Complex.I) * ∫ (σ : ℝ) in σ₁..1 + (Real.log X)⁻¹, SmoothedChebyshevIntegrand SmoothingF ε X (↑σ + ↑T * Complex.I)

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

Equations

• I₉ SmoothingF ε X T = 1 / (2 * ↑Real.pi * Complex.I) * (Complex.I * ∫ (t : ℝ) in Set.Ici T, SmoothedChebyshevIntegrand SmoothingF ε X (1 + ↑(Real.log X)⁻¹ + ↑t * Complex.I))

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

Equations

• I₃ SmoothingF ε T X σ₁ = 1 / (2 * ↑Real.pi * Complex.I) * (Complex.I * ∫ (t : ℝ) in -T..-3, SmoothedChebyshevIntegrand SmoothingF ε X (↑σ₁ + ↑t * Complex.I))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

def LogDerivZetaHasBound (A C : ℝ) : Prop

Equations

• LogDerivZetaHasBound A C = ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ici (1 - A / Real.log |t| ^ 9) → ‖deriv riemannZeta (↑σ + ↑t * Complex.I) / riemannZeta (↑σ + ↑t * Complex.I)‖ ≤ C * Real.log |t| ^ 9

def LogDerivZetaIsHoloSmall (σ₂ : ℝ) : Prop

Equations

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

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

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

theorem 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 BddAboveOnRect {g : ℂ → ℂ} {z w : ℂ} (holoOn : HolomorphicOn g (z.Rectangle w)) : BddAbove (norm ∘ g '' z.Rectangle w)

theorem 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 interval_membership (r a b : ℝ) (h1 : r ∈ Set.Icc (min a b) (max a b)) (h2 : a < b) : a ≤ r ∧ r ≤ b

theorem 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 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 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 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 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 poisson_kernel_integrable (x : ℝ) (hx : x ≠ 0) : MeasureTheory.Integrable (fun (t : ℝ) => (‖↑x + ↑t * Complex.I‖ ^ 2)⁻¹) MeasureTheory.volume

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

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

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

theorem 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) : ∃ C > 0, ∀ (ε : ℝ), 0 < ε → ε < 1 → ∀ (X : ℝ), 3 < X → ∀ {T : ℝ}, 3 < T → ‖I₁ SmoothingF ε X T‖ ≤ C * X * Real.log X / (ε * T)

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

theorem 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) : ∃ C > 0, ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ (X : ℝ), 3 < X → ∀ {T : ℝ}, 3 < T → ‖I₉ SmoothingF ε X T‖ ≤ C * X * Real.log X / (ε * T)

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

theorem I2Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {A C₂ : ℝ} (has_bound : LogDerivZetaHasBound A C₂) (C₂pos : 0 < C₂) (A_in : A ∈ Set.Ioc 0 (1 / 2)) : ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → have σ₁ := 1 - A / Real.log T ^ 9; ‖I₂ SmoothingF ε T X σ₁‖ ≤ C * X / (ε * T)

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

theorem I8Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {A C₂ : ℝ} (has_bound : LogDerivZetaHasBound A C₂) (C₂_pos : 0 < C₂) (A_in : A ∈ Set.Ioc 0 (1 / 2)) : ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → have σ₁ := 1 - A / Real.log T ^ 9; ‖I₈ SmoothingF ε T X σ₁‖ ≤ C * X / (ε * T)

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

theorem I3Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {A Cζ : ℝ} (hCζ : LogDerivZetaHasBound A Cζ) (Cζpos : 0 < Cζ) (hA : A ∈ Set.Ioc 0 (1 / 2)) : ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → have σ₁ := 1 - A / Real.log T ^ 9; ‖I₃ SmoothingF ε T X σ₁‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

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

theorem I7Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {A Cζ : ℝ} (hCζ : LogDerivZetaHasBound A Cζ) (Cζpos : 0 < Cζ) (hA : A ∈ Set.Ioc 0 (1 / 2)) : ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → have σ₁ := 1 - A / Real.log T ^ 9; ‖I₇ SmoothingF ε T X σ₁‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

theorem I4Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Set.Ioo 0 1) {A : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) : ∃ (C : ℝ) (_ : 0 ≤ C) (Tlb : ℝ) (_ : 3 < Tlb), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, Tlb < T → have σ₁ := 1 - A / Real.log T ^ 9; ‖I₄ SmoothingF ε X σ₁ σ₂‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

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

theorem I6Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Set.Ioo 0 1) {A : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) : ∃ (C : ℝ) (_ : 0 ≤ C) (Tlb : ℝ) (_ : 3 < Tlb), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, Tlb < T → have σ₁ := 1 - A / Real.log T ^ 9; ‖I₆ SmoothingF ε X σ₁ σ₂‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

theorem I5Bound {SmoothingF : ℝ → ℝ} (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Set.Ioo 0 1) : ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ‖I₅ SmoothingF ε X σ₂‖ ≤ C * X ^ σ₂ / ε

theorem LogDerivZetaBoundedAndHolo : ∃ (A : ℝ) (C : ℝ), 0 < C ∧ A ∈ Set.Ioc 0 (1 / 2) ∧ LogDerivZetaHasBound A C ∧ ∀ (T : ℝ), 3 ≤ T → HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.Icc (1 - A / Real.log T ^ 9) 2 ×ℂ Set.Icc (-T) T \ {1})

theorem 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 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 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.