English
HasFPowerSeriesWithinAt f p s x is equivalent to the existence of a local extension g that matches f on insert x s and HasFPowerSeriesAt g p x.
Русский
Существование рядов функции внутри точки эквивалентности находит локальное продолжение g, которое совпадает с f на insert x s и имеет ряд мощности в точке x.
LaTeX
$$$HasFPowerSeriesWithinAt f p s x \iff \exists g, f =^\mathrm{ᶠ}[𝓝[insert x s] x] g \land HasFPowerSeriesAt g p x$$$
Lean4
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series -/
theorem hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt [CompleteSpace F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} :
HasFPowerSeriesWithinAt f p s x ↔ ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x :=
by
constructor
· intro ⟨r, h⟩
rcases hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mp h with ⟨g, e, h⟩
refine ⟨g, ?_, ⟨r, h⟩⟩
refine Filter.eventuallyEq_iff_exists_mem.mpr ⟨_, ?_, e⟩
exact inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ h.r_pos)
· intro ⟨g, hfg, ⟨r, hg⟩⟩
simp only [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff] at hfg
rcases hfg with ⟨e, e0, hfg⟩
refine ⟨min r (.ofReal e), ?_⟩
refine hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨g, ?_, ?_⟩
· intro y ⟨ys, xy⟩
refine hfg ?_ ys
simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal] at xy
exact xy.2
· exact hg.mono (lt_min hg.r_pos (by positivity)) (min_le_left _ _)
