English
If HasFPowerSeriesWithinOnBall f p s x r and g agrees with f on ball x r, then HasFPowerSeriesWithinOnBall g p s x r.
Русский
Если у f есть степенной ряд внутри шара, и g совпадает с f на шаре x r, то у g тот же ряд.
LaTeX
$$$HasFPowerSeriesWithinOnBall\ f\ p\ s\ x\ r \Rightarrow EqOn f g (EMetric.ball x r) \Rightarrow HasFPowerSeriesWithinOnBall\ g\ p\ s\ x\ r$$
Lean4
/-- Variant of `HasFPowerSeriesWithinOnBall.congr` in which one requests equality on `insert x s`
instead of separating `x` and `s`. -/
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 (insert x s ∩ EMetric.ball x r)) :
HasFPowerSeriesWithinOnBall g p s x r :=
by
refine ⟨h.r_le, h.r_pos, fun {y} hy h'y ↦ ?_⟩
convert h.hasSum hy h'y using 1
exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩
