BKLNW_app.continuous_besselI0

lemma continuous_besselI0 : Continuous besselI0 := by  rw [continuous_iff_continuousAt]  intro x₀  have hmem : Metric.ball (0 : ℝ) (|x₀| + 1) ∈ nhds x₀ := by    refine Metric.isOpen_ball.mem_nhds ?_    simp only [Metric.mem_ball, Real.dist_eq, sub_zero]    linarith [abs_nonneg x₀]  refine (continuousOn_tsum    (fun m ↦ (((continuous_id.div_const 2).pow (2 * m)).div_const _).continuousOn)    (besselI0_summable (|x₀| + 1)) ?_).continuousAt hmem  intro m x hx  simp only [Metric.mem_ball, Real.dist_eq, sub_zero] at hx  have hb : |x / 2| ≤ (|x₀| + 1) / 2 := by    rw [abs_div, abs_two]    linarith  simp only [Pi.pow_apply, id_eq]  rw [Real.norm_eq_abs, abs_div, abs_pow, abs_pow,    abs_of_nonneg (by positivity : (0 : ℝ) ≤ ((m.factorial : ℝ)))]  gcongr