fderivWithin_star — Mathlib

English

The derivative within s of the star of f equals the star-linear map composed with the derivative within s of f.

Русский

Производная внутри s от star(f) равна star-линейному отображению, композиции со производной f внутри s.

LaTeX

$$$\\text{fderivWithin}_{\\mathbb{K}}(\\mathrm{star} \\circ f)\\; s\\; x = (\\mathrm{starL'}_{\\mathbb{K}}) \\circ_L \\text{fderivWithin}_{\\mathbb{K}}(f)\\; s\\; x$$$

Lean4

theorem fderivWithin_star (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun y => star (f y)) s x = ((starL' 𝕜 : F ≃L[𝕜] F) : F →L[𝕜] F) ∘L fderivWithin 𝕜 f s x :=
  (starL' 𝕜 : F ≃L[𝕜] F).comp_fderivWithin hxs

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