fderiv_star — Mathlib

English

Derivative of star(f) equals starL' composed with derivative of f.

Русский

Производная от star(f) равна композиции starL' с производной f.

LaTeX

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

Lean4

@[simp]
theorem fderiv_star : fderiv 𝕜 (fun y => star (f y)) x = ((starL' 𝕜 : F ≃L[𝕜] F) : F →L[𝕜] F) ∘L fderiv 𝕜 f x :=
  (starL' 𝕜 : F ≃L[𝕜] F).comp_fderiv

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