compContinuousLinearMap — Mathlib

English

If HasFPowerSeriesWithinOnBall f pf s (u x) r holds, then HasFPowerSeriesWithinOnBall (f ∘ u) (pf.compContinuousLinearMap u) (u⁻¹' s) x (r / ‖u‖)

Русский

Если есть ряд вокруг u x, то для композиции f ∘ u существует ряд вокруг x, радиус уменьшается на норму u.

LaTeX

$$HasFPowerSeriesWithinOnBall f pf s (ContinuousLinearMap.funLike.coe u x) r → HasFPowerSeriesWithinOnBall (Function.comp f (ContinuousLinearMap.funLike.coe u)) (pf.compContinuousLinearMap u) (Set.preimage (ContinuousLinearMap.funLike.coe u) s) x (instHDiv.hDiv r (SeminormedAddGroup.toContinuousENorm.enorm u))$$

Lean4

theorem compContinuousLinearMap (hf : HasFPowerSeriesAt f pf (u x)) :
    HasFPowerSeriesAt (f ∘ u) (pf.compContinuousLinearMap u) x :=
  let ⟨r, hr⟩ := hf
  ⟨r / ‖u‖ₑ, hr.compContinuousLinearMap⟩

Похожие утверждения