English
If a finite truncation data (finite, pos, sum_eq) hold for a function f around x with respect to a formal multilinear series p, then there exists a finite power series on the ball representing f around x.
Русский
Если даны условия (finite, pos, sum_eq) для функции f вокруг x относительно ряда p, существует конечный степенной ряд на ball, представляющий f вокруг x.
LaTeX
$$$(\forall m, n : \mathbb{N}, (finite) (pos) (sum\_eq)) \Rightarrow HasFiniteFPowerSeriesOnBall f p x n r$$$
Lean4
theorem congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ℝ≥0∞}
(h : HasFPowerSeriesWithinOnBall f p s x r) (h' : EqOn g f (s ∩ EMetric.ball x r)) (h'' : g x = f x) :
HasFPowerSeriesWithinOnBall g p s x r := by
refine ⟨h.r_le, h.r_pos, ?_⟩
intro y hy h'y
convert h.hasSum hy h'y using 1
simp only [mem_insert_iff, add_eq_left] at hy
rcases hy with rfl | hy
· simpa using h''
· apply h'
refine ⟨hy, ?_⟩
simpa [edist_eq_enorm_sub] using h'y
