comp_hasFDerivAt — Mathlib

English

The chain rule holds at the filter level: HasFDerivAtFilter for g ∘ f given HasFDerivAtFilter for g and HasFDerivAtFilter for f, with derivative composition.

Русский

Цепное правило справедливо для фильтров: производная композиции g∘f существует и задаётся композицией производных.

LaTeX

$$$\text{HasFDerivAtFilter}(g\circ f) = g'\circ f' + \cdot$$$

Lean4

theorem comp_hasFDerivAt {g : F → G} {g' : F →L[𝕜] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x))
    (hf : HasFDerivAt f f' x) (ht : ∀ᶠ x' in 𝓝 x, f x' ∈ t) : HasFDerivAt (g ∘ f) (g' ∘L f') x :=
  HasFDerivAtFilter.comp x hg hf <| tendsto_nhdsWithin_iff.mpr ⟨hf.continuousAt, ht⟩

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