English
If f has a power series on ball, then it continues to hold for all smaller radius r'.
Русский
Если у f есть степенной ряд на шаре, то радиус можно уменьшать; свойство сохраняется.
LaTeX
$$$HasFPowerSeriesOnBall\ f\ p\ x\ r \Rightarrow HasFPowerSeriesOnBall\ f\ p\ x\ r' \, (0 < r') \, (r' \le r)$$$
Lean4
theorem congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E}
(h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) : HasFPowerSeriesWithinAt g p s x :=
by
rcases h with ⟨r, hr⟩
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, EMetric.ball x ε ∩ s ⊆ {y | g y = f y} := EMetric.mem_nhdsWithin_iff.1 h'
let r' := min r ε
refine ⟨r', ?_⟩
have := hr.of_le (r' := r') (by simp [r', εpos, hr.r_pos]) (min_le_left _ _)
apply this.congr _ h''
intro z hz
exact hε ⟨EMetric.ball_subset_ball (min_le_right _ _) hz.2, hz.1⟩
