def mellintransform2 : Lean.ParserDescr

Equations

• mellintransform2 = Lean.ParserDescr.node `mellintransform2 1024 (Lean.ParserDescr.symbol "𝓜")

noncomputable def ChebyshevPsi (x : ℝ) : ℝ

Equations

• ChebyshevPsi x = (Finset.range ⌊x + 1⌋₊).sum ⇑ArithmeticFunction.vonMangoldt

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 * MellinTransform (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 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 : ℝ) => MellinTransform (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) * MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (↑σ + ↑t * Complex.I) * ↑X ^ (↑σ + ↑t * Complex.I) = ∑' (n : ℕ), ∫ (t : ℝ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ (↑σ + ↑t * Complex.I) * MellinTransform (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)) - ↑((Finset.range ⌊X + 1⌋₊).sum ⇑ArithmeticFunction.vonMangoldt)‖ ≤ 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 : ℝ), ∀ (X : ℝ), 3 < X → ∀ (ε : ℝ), 0 < ε → ε < 1 → 2 < X * ε → ‖SmoothedChebyshev SmoothingF ε X - ↑(ChebyshevPsi 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

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

theorem summable_real_iff_summable_coe_complex (f : ℕ → ℝ) : Summable f ↔ Summable fun (n : ℕ) => ↑(f n)

theorem cast_pow_eq (n : ℕ) (σ₀ : ℝ) : ↑(↑n ^ σ₀) = ↑n ^ ↑σ₀

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

theorem analyticAt_riemannZeta {s : ℂ} (s_ne_one : s ≠ 1) : AnalyticAt ℂ riemannZeta s

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

theorem differentiableAt_deriv_riemannZeta {s : ℂ} (s_ne_one : s ≠ 1) : DifferentiableAt ℂ (deriv riemannZeta) s

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 + MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) 1 * ↑X

theorem SmoothedChebyshevPull2 {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (ε_lt_one : ε < 1) (X : ℝ) : 3 < X → ∀ {T : ℝ} (T_pos : 0 < 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), 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 → ‖MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) 1 * ↑X - ↑X‖ ≤ C * ε * X

theorem IBound_aux1 {k : ℝ} (k_pos : 0 < k) : ∃ C > 0, ∀ {T : ℝ}, 3 < T → Real.log T ^ k ≤ C * T

theorem I1Bound : ∃ C > 0, ∀ {SmoothingF : ℝ → ℝ} {ε : ℝ}, 0 < ε → ε < 1 → ∀ (X : ℝ), 3 < X → ∀ {T : ℝ}, 3 < T → ∀ {σ₁ : ℝ}, Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → ‖I₁ SmoothingF ε X T‖ ≤ C * X * Real.log X / (ε * T)

theorem I9Bound : ∃ C > 0, ∀ {SmoothingF : ℝ → ℝ} {ε : ℝ}, 0 < ε → ε < 1 → ∀ (X : ℝ), 3 < X → ∀ {T : ℝ}, 3 < T → ∀ {σ₁ : ℝ}, Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → ‖I₉ SmoothingF ε X T‖ ≤ C * X * Real.log X / (ε * T)

theorem I2Bound : ∃ (C : ℝ) (_ : 0 < C) (A : ℝ) (_ : A ∈ Set.Ioo 0 (1 / 2)), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → let σ₁ := 1 - A / Real.log X ^ 9; ‖I₂ SmoothingF ε X T σ₁‖ ≤ C * X / (ε * T)

theorem I8Bound : ∃ (C : ℝ) (_ : 0 < C) (A : ℝ) (_ : A ∈ Set.Ioo 0 (1 / 2)), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → let σ₁ := 1 - A / Real.log X ^ 9; ‖I₈ SmoothingF ε X T σ₁‖ ≤ C * X / (ε * T)

theorem I3Bound : ∃ (C : ℝ) (_ : 0 < C) (A : ℝ) (_ : A ∈ Set.Ioo 0 (1 / 2)), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → let σ₁ := 1 - A / Real.log X ^ 9; ‖I₃ SmoothingF ε X T σ₁‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

theorem I7Bound : ∃ (C : ℝ) (_ : 0 < C) (A : ℝ) (_ : A ∈ Set.Ioo 0 (1 / 2)), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → let σ₁ := 1 - A / Real.log X ^ 9; ‖I₇ SmoothingF ε X T σ₁‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

theorem I4Bound : ∃ (C : ℝ) (_ : 0 < C) (A : ℝ) (_ : A ∈ Set.Ioo 0 (1 / 2)) (σ₂ : ℝ) (_ : σ₂ ∈ Set.Ioo 0 1), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → let σ₁ := 1 - A / Real.log X ^ 9; ‖I₄ SmoothingF ε X σ₁ σ₂‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

theorem I6Bound : ∃ (C : ℝ) (_ : 0 < C) (A : ℝ) (_ : A ∈ Set.Ioo 0 (1 / 2)) (σ₂ : ℝ) (_ : σ₂ ∈ Set.Ioo 0 1), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → ∀ {T : ℝ}, 3 < T → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → let σ₁ := 1 - A / Real.log X ^ 9; ‖I₆ SmoothingF ε X σ₁ σ₂‖ ≤ C * X * X ^ (-A / Real.log T ^ 9) / ε

theorem I5Bound : ∃ (C : ℝ) (_ : 0 < C) (σ₂ : ℝ) (_ : σ₂ ∈ Set.Ioo 0 1), ∀ {SmoothingF : ℝ → ℝ} (X : ℝ), 3 < X → ∀ {ε : ℝ}, 0 < ε → ε < 1 → Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2 → (∀ x > 0, 0 ≤ SmoothingF x) → ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1 → ContDiff ℝ 1 SmoothingF → ‖I₅ SmoothingF ε X σ₂‖ ≤ C * X ^ σ₂ / ε

theorem MediumPNT : ∃ c > 0, (ChebyshevPsi - 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.