logDeriv_comp — Mathlib

English

The log-derivative of a composition f ∘ g satisfies logDeriv(f ∘ g)(x) = logDeriv f(g(x)) · deriv g(x).

Русский

Логарифмическая производная композиции f ∘ g удовлетворяет: logDeriv(f ∘ g)(x) = logDeriv f(g(x)) · g'(x).

LaTeX

$$$\displaystyle \logDeriv\bigl(f \circ g\bigr)(x) = \logDeriv f\bigl(g(x)\bigr) \cdot \bigl(\operatorname{deriv} g(x)\bigr)$$$

Lean4

theorem logDeriv_comp {f : 𝕜' → 𝕜'} {g : 𝕜 → 𝕜'} {x : 𝕜} (hf : DifferentiableAt 𝕜' f (g x))
    (hg : DifferentiableAt 𝕜 g x) : logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x :=
  by
  simp only [logDeriv, Pi.div_apply, deriv_comp _ hf hg, comp_apply]
  ring

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