norm_expSeries_summable_of_mem_ball'

English

Same as above for the primed variant.

Русский

То же самое для производной версии.

LaTeX

$$Summable \\|expSeries 𝕂 𝔸 n (fun _ => x)\\|$$

Lean4

theorem norm_expSeries_summable_of_mem_ball' (x : 𝔸) (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    Summable fun n => ‖(n !⁻¹ : 𝕂) • x ^ n‖ :=
  by
  change Summable (norm ∘ _)
  rw [← expSeries_apply_eq']
  exact norm_expSeries_summable_of_mem_ball x hx

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