English
If f and g are open-neighborhood congruent on s, then AnalyticOnNhd 𝕜 f s ⇔ AnalyticOnNhd 𝕜 g s.
Русский
Если f и g совпадают на окрестности по s, аналитичность на окрестности совпадает.
LaTeX
$$$\text{IsOpen}(s) \land s.EqOn(f,g) \Rightarrow \text{AnalyticOnNhd}_{\mathcal{K}}(f,s) \iff \text{AnalyticOnNhd}_{\mathcal{K}}(g,s)$$$
Lean4
/-- If a function `f` has a power series `p` on a ball within a set and `g` is linear,
then `g ∘ f` has the power series `g ∘ p` on the same ball. -/
theorem comp_hasFPowerSeriesWithinOnBall (g : F →L[𝕜] G) (h : HasFPowerSeriesWithinOnBall f p s x r) :
HasFPowerSeriesWithinOnBall (g ∘ f) (g.compFormalMultilinearSeries p) s x r
where
r_le := h.r_le.trans (p.radius_le_radius_continuousLinearMap_comp _)
r_pos := h.r_pos
hasSum hy
h'y := by
simpa only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply] using g.hasSum (h.hasSum hy h'y)
