def mellintransform2 : Lean.ParserDescr

Equations

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

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) 2

theorem Smooth1_AEStronglyMeasurable {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (ε : ℝ) (εpos : 0 < ε) : MeasureTheory.AEStronglyMeasurable (Smooth1 SmoothingF ε) MeasureTheory.volume

theorem integrable_x_mul_Smooth1 {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ (x : ℝ), 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) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x * Smooth1 SmoothingF ε x) (Set.Ioi 0) MeasureTheory.volume

theorem vertical_integrable_Smooth1 {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ (x : ℝ), 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 < ε) : MeasureTheory.Integrable (fun (y : ℝ) => ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (1 + ↑y * Complex.I) * ↑(Smooth1 SmoothingF ε t)) MeasureTheory.volume

theorem continuousAt_Smooth1 {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ (x : ℝ), 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 < ε) (y : ℝ) (ypos : 0 < y) : ContinuousAt (fun (x : ℝ) => Smooth1 SmoothingF ε x) y

theorem SmoothedChebyshevDirichlet {SmoothingF : ℝ → ℝ} (diffSmoothingF : ContDiff ℝ 1 SmoothingF) (SmoothingFpos : ∀ (x : ℝ), 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) : SmoothedChebyshev SmoothingF ε X = ↑(∑' (n : ℕ), ArithmeticFunction.vonMangoldt n * Smooth1 SmoothingF ε (↑n / X))

noncomputable def ChebyshevPsi (x : ℝ) : ℝ

Equations

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

theorem SmoothedChebyshevClose {SmoothingF : ℝ → ℝ} (ε : ℝ) (ε_pos : 0 < ε) (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) (X : ℝ) : (fun (X : ℝ) => ‖SmoothedChebyshev SmoothingF ε X - ↑(ChebyshevPsi X)‖) =O[Filter.atTop] fun (X : ℝ) => ε * X * Real.log X

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

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