Equations
- mellintransform2 = Lean.ParserDescr.node `mellintransform2 1024 (Lean.ParserDescr.symbol "𝓜")
@[reducible, inline]
Equations
- SmoothedChebyshevIntegrand SmoothingF ε X s = -deriv riemannZeta s / riemannZeta s * MellinTransform (fun (x : ℝ) => ↑(Smooth1 SmoothingF ε x)) s * ↑X ^ s
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))
Equations
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))