Source indexedtheorem · leanprover/lean4:v4.32.0

I9Bound

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2150 to 2164

Mathematical statement

Exact Lean statement

theorem I9Bound
    {SmoothingF : ℝ → ℝ}
    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF)
    (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x)
    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1) :
    ∃ C > 0, ∀{ε : ℝ} (_ : 0 < ε)
    (_ : ε < 1)
    (X : ℝ) (_ : 3 < X)
    {T : ℝ} (_ : 3 < T),
    ‖I₉ SmoothingF ε X T‖ ≤ C * X * Real.log X / (ε * T)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem I9Bound    {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2) (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF)    (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x)    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1) :    ∃ C > 0, ∀{ε : ℝ} (_ : 0 < ε)    (_ : ε < 1)    (X : ℝ) (_ : 3 < X)    {T : ℝ} (_ : 3 < T),    ‖I₉ SmoothingF ε X T‖ ≤ C * X * Real.log X / (ε * T) := by  obtain ⟨C, Cpos, bound⟩ := I1Bound suppSmoothingF ContDiffSmoothingF SmoothingFnonneg mass_one  refine ⟨C, Cpos, ?_⟩  intro ε εpos ε_lt_one X X_gt T T_gt  specialize bound ε εpos ε_lt_one X X_gt T_gt  rwa [I9I1 (by linarith), norm_conj]