English
A power series expansion of f around x on the ball of radius r within s exists iff there is a local extension g that agrees with f on insert x s and has a power series on ball around x of radius r.
Русский
Ро́зложение в ряд Фурье/многочленных коэффициентов вокруг точки x внутри ball(x,r) существует для f на s тогда и только тогда, когда существует локальное продолжение g, совпадающее с f на insert x s и обладающее рядом мощности на ball(x,r).
LaTeX
$$$HasFPowerSeriesWithinOnBall f p s x r \iff \exists g, EqOn f g (insert x s \cap EMetric.ball x r) \land HasFPowerSeriesOnBall g p x r$$$
Lean4
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series -/
theorem hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpace F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ℝ≥0∞} :
HasFPowerSeriesWithinOnBall f p s x r ↔
∃ g, EqOn f g (insert x s ∩ EMetric.ball x r) ∧ HasFPowerSeriesOnBall g p x r :=
by
constructor
· intro h
refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
· intro y ⟨ys, yb⟩
simp only [EMetric.mem_ball, edist_eq_enorm_sub] at yb
have e0 := p.hasSum (x := y - x) ?_
have e1 := (h.hasSum (y := y - x) ?_ ?_)
· simp only [add_sub_cancel] at e1
exact e1.unique e0
· simpa only [add_sub_cancel]
· simpa only [EMetric.mem_ball, edist_zero_eq_enorm]
· simp only [EMetric.mem_ball, edist_zero_eq_enorm]
exact lt_of_lt_of_le yb h.r_le
· refine ⟨h.r_le, h.r_pos, ?_⟩
intro y lt
simp only [add_sub_cancel_left]
apply p.hasSum
simp only [EMetric.mem_ball] at lt ⊢
exact lt_of_lt_of_le lt h.r_le
· intro ⟨g, hfg, hg⟩
refine ⟨hg.r_le, hg.r_pos, ?_⟩
intro y ys lt
rw [hfg]
· exact hg.hasSum lt
· refine ⟨ys, ?_⟩
simpa only [EMetric.mem_ball, edist_eq_enorm_sub, add_sub_cancel_left, sub_zero] using lt
