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 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) : MeasureTheory.Integrable (fun (y : ℝ) => MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (2 + ↑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) : ∫ (t : ℝ), ∑' (n : ℕ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ (2 + ↑t * Complex.I) * MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (2 + ↑t * Complex.I) * ↑X ^ (2 + ↑t * Complex.I) = ∑' (n : ℕ), ∫ (t : ℝ), ↑(ArithmeticFunction.vonMangoldt n) / ↑n ^ (2 + ↑t * Complex.I) * MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) (2 + ↑t * Complex.I) * ↑X ^ (2 + ↑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_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 : ℝ → ℝ} (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) (X : ℝ) : ∃ (C : ℝ) (_ : 0 < C), ∀ (X : ℝ), C < X → ∀ (ε : ℝ), 0 < ε → ε < 1 → ‖SmoothedChebyshev SmoothingF ε X - ↑(ChebyshevPsi X)‖ ≤ C * ε * X * Real.log X

theorem SmoothedChebyshevPull1_aux_integrable {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (X : ℝ) {σ₀ : ℝ} (σ₀_pos : 0 < σ₀) (holoOn : HolomorphicOn (SmoothedChebyshevIntegrand SmoothingF ε X) (Set.Icc σ₀ 2 ×ℂ Set.univ \ {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) : MeasureTheory.Integrable (fun (t : ℝ) => SmoothedChebyshevIntegrand SmoothingF ε X (2 + ↑t * Complex.I)) MeasureTheory.volume

theorem SmoothedChebyshevPull1 {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (X : ℝ) {T : ℝ} (T_pos : 0 < T) {σ₀ : ℝ} (σ₀_pos : 0 < σ₀) (holoOn : HolomorphicOn (SmoothedChebyshevIntegrand SmoothingF ε X) (Set.Icc σ₀ 2 ×ℂ Set.univ \ {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) : SmoothedChebyshev SmoothingF ε X = MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) 1 * ↑X + 1 / (2 * ↑Real.pi * Complex.I) * (((((Complex.I * ∫ (t : ℝ) in Set.Iic (-T), SmoothedChebyshevIntegrand SmoothingF ε X (2 + ↑t * Complex.I)) - ∫ (s : ℝ) in Set.Icc σ₀ 2, SmoothedChebyshevIntegrand SmoothingF ε X (↑s - ↑T * Complex.I)) + Complex.I * ∫ (t : ℝ) in Set.Icc (-T) T, SmoothedChebyshevIntegrand SmoothingF ε X (↑σ₀ + ↑t * Complex.I)) + ∫ (s : ℝ) in Set.Icc σ₀ 2, SmoothedChebyshevIntegrand SmoothingF ε X (↑s + ↑T * Complex.I)) + Complex.I * ∫ (t : ℝ) in Set.Ici T, SmoothedChebyshevIntegrand SmoothingF ε X (2 + ↑t * Complex.I))

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