English
If a HasFPowerSeriesWithinOnBall f pf s (u x) r holds, then the composition f ∘ u has a power series within ball with coefficients pf.compContinuousLinearMap u on Set.preimage (f x) and radius r adjusted by the operator norm of u.
Русский
Если имеем HadFPowerSeriesWithinOnBall f pf s вокруг (u x) с радиусом r, то композиция f ∘ u имеет ряд в шаре с коэффициентами pf.compContinuousLinearMap u на предобразном множестве и радиусе, поделённом на норму u.
LaTeX
$$HasFPowerSeriesWithinOnBall f pf s (ContinuousLinearMap.funLike.coe u x) r → HasFPowerSeriesWithinOnBall (f ∘ u) (pf.compContinuousLinearMap u) (Set.preimage (ContinuousLinearMap.funLike.coe u) s) x (r / ‖u‖ₑ)$$
Lean4
theorem unshift (hf : HasFPowerSeriesWithinAt f pf s x) :
HasFPowerSeriesWithinAt (fun y ↦ z + f y (y - x)) (pf.unshift z) s x :=
let ⟨_, hrf⟩ := hf
hrf.unshift.hasFPowerSeriesWithinAt
