Documentation

PrimeNumberTheoremAnd.MediumPNT

@[reducible, inline]
noncomputable abbrev SmoothedChebyshevIntegrand (SmoothingF : ) (ε X : ) :
Equations
noncomputable def SmoothedChebyshev (SmoothingF : ) (ε X : ) :
Equations
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))
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 < εε < 1SmoothedChebyshev 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) :
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.