expSeries_hasSum_exp_of_mem_ball'

English

For x in the ball, the expSeries has sum exp x.

Русский

Для x внутри шара expSeries суммируется в exp x.

LaTeX

$$HasSum (fun n => expSeries 𝕂 𝔸 n fun _ => x) (exp 𝕂 x)$$

Lean4

theorem expSeries_hasSum_exp_of_mem_ball' (x : 𝔸) (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasSum (fun n => (n !⁻¹ : 𝕂) • x ^ n) (exp 𝕂 x) :=
  by
  rw [← expSeries_apply_eq']
  exact expSeries_hasSum_exp_of_mem_ball x hx

Похожие утверждения