hasFPowerSeriesWithinOnBall_pi_iff

English

Equality of pi-radius with iInf-radius via has equality.

Русский

Радиус pi равен inf радиусу через iInf.

LaTeX

$$$(FormalMultilinearSeries.pi p).radius = \\bigsqcap_i (p i).radius$$$

Lean4

theorem hasFPowerSeriesWithinOnBall_pi_iff (hr : 0 < r) :
    HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r ↔
      ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r
    where
  mp h i := ⟨h.r_le.trans (FormalMultilinearSeries.radius_pi_le _ _), hr, fun m hy ↦ Pi.hasSum.1 (h.hasSum m hy) i⟩
  mpr h := .pi h hr

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