hasFiniteFPowerSeriesOnBall_of_finite

English

A finite formal multilinear series yields a finite power-series on a ball; i.e., HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤ when p is finite.

Русский

Конечная формальная линейная серия задаёт конечный степенной ряд на шаре; то есть HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤ при конечности p.

LaTeX

$$HasFiniteFPowerSeriesOnBall\\ p.sum\\ p\\ 0\\ n\\ ⊤$$

Lean4

/-- The sum of a finite power series `p` admits `p` as a power series. -/
protected theorem hasFiniteFPowerSeriesOnBall_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ m, n ≤ m → p m = 0) : HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤
    where
  r_le := by rw [radius_eq_top_of_forall_image_add_eq_zero p n fun _ => hn _ (Nat.le_add_left _ _)]
  r_pos := zero_lt_top
  finite := hn
  hasSum {y} _ := by rw [zero_add]; exact p.hasSum_of_finite hn y

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