English
A net f_i of power series tends to g in the Pi-topology iff for every d, the coefficients d of f_i tend to the coefficient d of g.
Русский
Сходимость семейства степенных рядов по топологии Pi эквивалентна сходимости по каждому коэффициенту: для каждого d последовательность coeff_d(f_i) сходится к coeff_d(g).
LaTeX
$$$ \\text{Tendsto}(f,u,nhds(g)) \\iff \\forall d, \\text{Tendsto}(i \\mapsto \\operatorname{coeff}_d(f(i))) \\; u \\; nhds(\\operatorname{coeff}_d(g)). $$$
Lean4
/-- A family of power series converges iff it converges coefficientwise -/
theorem tendsto_iff_coeff_tendsto [Semiring R] {ι : Type*} (f : ι → PowerSeries R) (u : Filter ι) (g : PowerSeries R) :
Tendsto f u (nhds g) ↔ ∀ d : ℕ, Tendsto (fun i => coeff d (f i)) u (nhds (coeff d g)) :=
by
rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]
apply (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.forall_congr
intro d
simp only [LinearEquiv.coe_toEquiv, Finsupp.LinearEquiv.finsuppUnique_apply, PUnit.default_eq_unit, coeff]
apply iff_of_eq
congr
· ext _; congr; ext; simp
· ext; simp
