hasFPowerSeriesAt_iff' — Mathlib

English

HasFPowerSeriesAt f p z0 is equivalent to the property that near z0, f is the sum of the transformed coefficients of p.

Русский

Эквивалентно свойство, что около z0 функция f равна сумме коэффициентов p после преобразований.

LaTeX

$$$ HasFPowerSeriesAt f p z0 \Leftrightarrow \forall^\! z \in \nhds(z0), HasSum (fun n => (z-z0)^n • p.coeff n) (f z) $$$

Lean4

theorem hasFPowerSeriesAt_iff' :
    HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ z in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • p.coeff n) (f z) :=
  by
  rw [← map_add_left_nhds_zero, eventually_map, hasFPowerSeriesAt_iff]
  simp_rw [add_sub_cancel_left]

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