English
A power series expansion at z0 is zero near z0 if and only if all coefficients vanish; equivalently, the function is identically zero in a neighborhood of z0.
Русский
Разложение в степенной ряд около z0 равно нулю близко к z0 тогда и только тогда, когда все коэффициенты нулевые; эквивалентно, функция тождественно нулевая в некоторой окрестности z0.
LaTeX
$$$loc\!a\!l\!l p.radius > 0 \Rightarrow (f \text{ vanishes locally}) \iff p = 0$$$
Lean4
theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀)^[p.order] f z :=
by
have hq := hasFPowerSeriesAt_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
filter_upwards [hq, hasFPowerSeriesAt_iff'.mp hp] with x hx1 hx2
have : ∀ k < p.order, p.coeff k = 0 := fun k hk => by simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
obtain ⟨s, hs1, hs2⟩ := HasSum.exists_hasSum_smul_of_apply_eq_zero hx2 this
convert hs1.symm
simp only [coeff_iterate_fslope] at hx1
exact hx1.unique hs2
