log — Mathlib

English

Under differentiability within s, and f(x) ≠ 0 with unique-diff within s at x, the derivative within s of log∘f equals the quotient of the derivative within s of f by f(x).

Русский

При дифференцируемости внутри s и f(x) ≠ 0 с условием уникальной точки дифференциации, производная внутри s логарифма равна отношению производной к f(x).

LaTeX

$$derivWithin (log ∘ f) s x = derivWithin f s x / f x$$

Lean4

@[simp]
theorem log (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) : deriv (fun x => log (f x)) x = deriv f x / f x :=
  (hf.hasDerivAt.log hx).deriv

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