English
If a one-dimensional FM-series p represents the zero function at x, then p is identically zero.
Русский
Если одномерный FM-ряд p представляет нулевую функцию в точке x, то p тождественно равен нулю.
LaTeX
$$$\\text{HasFPowerSeriesAt}_{0}(p,x) \\Rightarrow p = 0.$$$
Lean4
/-- If a formal multilinear series `p` represents the zero function at `x : E`, then the
terms `p n (fun i ↦ y)` appearing in the sum are zero for any `n : ℕ`, `y : E`. -/
theorem apply_eq_zero {p : FormalMultilinearSeries 𝕜 E F} {x : E} (h : HasFPowerSeriesAt 0 p x) (n : ℕ) :
∀ y : E, (p n fun _ => y) = 0 :=
by
refine Nat.strong_induction_on n fun k hk => ?_
have psum_eq : p.partialSum (k + 1) = fun y => p k fun _ => y :=
by
funext z
refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_
· have := Finset.mem_range_succ_iff.mp hb
simp only [hk b (this.lt_of_ne hnb)]
· exact False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))
replace h := h.isBigO_sub_partialSum_pow k.succ
simp only [psum_eq, zero_sub, Pi.zero_apply, Asymptotics.isBigO_neg_left] at h
exact h.continuousMultilinearMap_apply_eq_zero
