log — Mathlib

English

If f has a within-set derivative f' at x and f(x) ≠ 0, then log ∘ f has derivative f'/f(x) within the same set.

Русский

Если f имеет внутри множества производную f' в точке x и f(x) ≠ 0, то log(f(x)) имеет внутри множества производную f(x)/f(x).

LaTeX

$$HasDerivWithinAt log (f x) (f' / f x) s x$$

Lean4

theorem log (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) : HasDerivWithinAt (fun y => log (f y)) (f' / f x) s x :=
  by
  rw [div_eq_inv_mul]
  exact (hasDerivAt_log hx).comp_hasDerivWithinAt x hf

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