English
A function f has a power series expansion at z0 iff it equals the sum of its coefficients in a neighborhood of z0.
Русский
У функции f есть разложение по степенному ряду в точке z0 тогда и только тогда, когда в окрестности z0 она равна сумме коэффициентов ряда.
LaTeX
$$$ HasFPowerSeriesAt f p z0 \Leftrightarrow \forall^{\!} z \text{ в } \mathcal{nhds}(z0), HasSum (fun n => z^n • p.coeff n) (f(z0+z)) $$$
Lean4
/-- A function `f : 𝕜 → E` has `p` as power series expansion at a point `z₀` iff it is the sum of
`p` in a neighborhood of `z₀`. This makes some proofs easier by hiding the fact that
`HasFPowerSeriesAt` depends on `p.radius`. -/
theorem hasFPowerSeriesAt_iff :
HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ z in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z)) :=
by
refine ⟨fun ⟨r, _, r_pos, h⟩ => eventually_of_mem (EMetric.ball_mem_nhds 0 r_pos) fun _ => by simpa using h, ?_⟩
simp only [Metric.eventually_nhds_iff]
rintro ⟨r, r_pos, h⟩
refine ⟨p.radius ⊓ r.toNNReal, by simp, ?_, ?_⟩
· simp only [r_pos.lt, lt_inf_iff, ENNReal.coe_pos, Real.toNNReal_pos, and_true]
obtain ⟨z, z_pos, le_z⟩ := NormedField.exists_norm_lt 𝕜 r_pos.lt
have : (‖z‖₊ : ENNReal) ≤ p.radius := by
simp only [dist_zero_right] at h
apply FormalMultilinearSeries.le_radius_of_tendsto
convert tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero
simp [norm_smul, mul_comm]
refine lt_of_lt_of_le ?_ this
simp only [ENNReal.coe_pos]
exact zero_lt_iff.mpr (nnnorm_ne_zero_iff.mpr (norm_pos_iff.mp z_pos))
· simp only [EMetric.mem_ball, lt_inf_iff, edist_lt_coe, apply_eq_pow_smul_coeff, and_imp, dist_zero_right] at h ⊢
refine fun {y} _ hyr => h ?_
simpa [nndist_eq_nnnorm, Real.lt_toNNReal_iff_coe_lt] using hyr
