English
At a point x, differentiability of the postcomposition with a fixed linear map carries differentiability of f at x to the postcomposed map.
Русский
В точке x дифференцируемость посткомпоновки сохраняется: если f дифференцируема в точке x, то посткомпонованное отображение дифференцируемо в x.
LaTeX
$$$$MDifferentiableAt I 𝓘(𝕜, F_2 \to_L[𝕜] F_3) f x \Rightarrow MDifferentiableAt I 𝓘(𝕜, (F_1 \to_L[𝕜] F_2) \to_L[𝕜] (F_1 \to_L[𝕜] F_3)) (\lambda y. (f(y)).postcomp F_1) x.$$$$
Lean4
theorem clm_postcomp {f : M → F₂ →L[𝕜] F₃} {x : M} (hf : MDifferentiableAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) f x) :
MDifferentiableAt I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃))
(fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) x :=
Differentiable.comp_mdifferentiableAt (ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃)) hf
