clm_postcomp — Mathlib

English

Global differentiability of the postcomposition map by a fixed linear operator when the original map is differentiable.

Русский

Глобальная дифференцируемость посткомпонования фиксированным линейным оператором при дифференцируемости исходного отображения.

LaTeX

$$$$\forall f: M \to F_2 \to_L F_3,\ MDifferentiable I 𝓘(𝕜, F_2 \to_L[𝕜] F_3) f \Rightarrow MDifferentiable I 𝓘(𝕜, (F_1 \to_L[𝕜] F_2) \to_L[𝕜] (F_1 \to_L[𝕜] F_3)) (\lambda y. (f y).postcomp F_1). $$$$

Lean4

theorem clm_postcomp {f : M → F₂ →L[𝕜] F₃} (hf : MDifferentiable I 𝓘(𝕜, F₂ →L[𝕜] F₃) f) :
    MDifferentiable I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃))
      (fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) :=
  fun x ↦ (hf x).clm_postcomp

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