Documentation

PrimeNumberTheoremAnd.MediumPNT

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