BKLNW_app.η_le

lemma η_le {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) (ξ : ℝ) :    η c ε ξ ≤ c / (2 * ε * sinh c) * besselI0 c := by  have hs : 0 < sinh c := sinh_pos_iff.mpr hc  have hcoef : 0 ≤ c / (2 * ε * sinh c) :=    div_nonneg hc.le (by nlinarith [mul_pos hε hs])  unfold η  split  · refine mul_le_mul_of_nonneg_left (besselI0_le_besselI0 ?_) hcoef    have h1 : sqrt (1 - (ξ / ε) ^ 2) ≤ 1 :=      Real.sqrt_le_one.mpr (by nlinarith [sq_nonneg (ξ / ε)])    calc |c * sqrt (1 - (ξ / ε) ^ 2)|        = c * sqrt (1 - (ξ / ε) ^ 2) :=          abs_of_nonneg (mul_nonneg hc.le (Real.sqrt_nonneg _))      _ ≤ c * 1 := mul_le_mul_of_nonneg_left h1 hc.le      _ = c := mul_one c      _ = |c| := (abs_of_pos hc).symm  · exact mul_nonneg hcoef (besselI0_nonneg c)