English
The radius of convergence of the exponential series is top (infinite).
Русский
Радиус сходимости ряда экспоненты бесконечен.
LaTeX
$$$ (\operatorname{expSeries} 𝕂 𝔸).radius = \infty $$$
Lean4
/-- In a normed algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, the series defining the exponential map
has an infinite radius of convergence. -/
theorem expSeries_radius_eq_top : (expSeries 𝕂 𝔸).radius = ∞ :=
by
have {n : ℕ} : (Nat.factorial n : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
apply expSeries_eq_ofScalars 𝕂 𝔸 ▸ ofScalars_radius_eq_top_of_tendsto 𝔸 _ (Eventually.of_forall fun n => ?_)
· simp_rw [← norm_div, Nat.factorial_succ, Nat.cast_mul, mul_inv_rev, mul_div_right_comm, inv_div_inv, norm_mul,
div_self this, norm_one, one_mul]
apply norm_zero (E := 𝕂) ▸ Filter.Tendsto.norm
apply (Filter.tendsto_add_atTop_iff_nat (f := fun n => (n : 𝕂)⁻¹) 1).mpr
exact RCLike.tendsto_inverse_atTop_nhds_zero_nat 𝕂
· simp [this]
