Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW_app.ν_abs_le

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1027 to 1037

Mathematical statement

Exact Lean statement

lemma ν_abs_le {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) (t : ℝ) :
    |ν c ε t| ≤ c / sinh c * besselI0 c * (2 * ε)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ν_abs_le {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) (t : ℝ) :    |ν c ε t| ≤ c / sinh c * besselI0 c * (2 * ε) := by  have hs : 0 < sinh c := sinh_pos_iff.mpr hc  have hM : 0 ≤ c / sinh c * besselI0 c :=    mul_nonneg (div_nonneg hc.le hs.le) (besselI0_nonneg c)  unfold ν  exact abs_setIntegral_Iic_le hε hM (fun x ↦ μ_abs_le hc hε x)    (fun x hx ↦ by      rcases lt_abs.mp hx with h1 | h1      · exact μ_eq_zero_of_gt hε h1      · exact μ_eq_zero_of_lt_neg hε (by linarith)) t