Source indexedlemma · leanprover/lean4:v4.32.0

I7Bound

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2990 to 3003

Mathematical statement

Exact Lean statement

lemma I7Bound {SmoothingF : ℝ → ℝ}
    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)
    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF)
    {A Cζ : ℝ} (hCζ : LogDerivZetaHasBound A Cζ) (Cζpos : 0 < Cζ) (hA : A ∈ Ioc 0 (1 / 2))
    : ∃ (C : ℝ) (_ : 0 < C),
    ∀ (X : ℝ) (_ : 3 < X) {ε : ℝ} (_ : 0 < ε)
    (_ : ε < 1) {T : ℝ} (_ : 3 < T),
    let σ₁ : ℝ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma I7Bound {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF)    {A Cζ : ℝ} (hCζ : LogDerivZetaHasBound A Cζ) (Cζpos : 0 < Cζ) (hA : A ∈ Ioc 0 (1 / 2))    : ∃ (C : ℝ) (_ : 0 < C),    ∀ (X : ℝ) (_ : 3 < X) {ε : ℝ} (_ : 0 < ε)    (_ : ε < 1) {T : ℝ} (_ : 3 < T),    let σ₁ : ℝ := 1 - A / (Real.log T) ^ 9    ‖I₇ SmoothingF ε T X σ₁‖ ≤ C * X * X ^ (- A / (Real.log T ^ 9)) / ε := by  obtain ⟨C, Cpos, bound⟩ := I3Bound suppSmoothingF ContDiffSmoothingF hCζ Cζpos hA  refine ⟨C, Cpos, fun X X_gt ε εpos ε_lt_one T T_gt ↦ ?_⟩  specialize bound X X_gt εpos ε_lt_one T_gt  intro σ₁  rwa [I7I3 (by linarith), norm_conj]