dslope_comp — Mathlib

English

For a composition f ∘ g, dslope equals f applied to dslope g, provided differentiability holds at a.

Русский

Для композиции f ∘ g dslope равен f( dslope g ), если дифференцируемость в a выполняется.

LaTeX

$$$ dslope (f \circ g) a b = f ( dslope g a b ) $ under suitable differentiability.$$

Lean4

theorem dslope_comp {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (g : 𝕜 → E) (a b : 𝕜)
    (H : a = b → DifferentiableAt 𝕜 g a) : dslope (f ∘ g) a b = f (dslope g a b) :=
  by
  rcases eq_or_ne b a with (rfl | hne)
  · simp only [dslope_same]
    exact (f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv
  · simpa only [dslope_of_ne _ hne] using f.toLinearMap.slope_comp g a b

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