clm_postcomp — Mathlib

English

On a set, differentiability of the postcomposition with a fixed linear map is preserved pointwise from f to f.postcomp F1.

Русский

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

LaTeX

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

Lean4

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

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