English
logDeriv of a quotient equals logDeriv f minus logDeriv g, under nonzero conditions and differentiability.
Русский
logDeriv частного равен разности logDeriv числителя и знаменателя при ненулевых значениях и дифференцируемости.
LaTeX
$$$\forall f,g:\; x:\mathbb{K},\; f(x)\neq 0,\; g(x)\neq 0,\; \text{DifferentiableAt } f x,\; \text{DifferentiableAt } g x\Rightarrow\logDeriv\,(f\,/\;g) x = \logDeriv f x - \logDeriv g x$$$
Lean4
theorem logDeriv_div {f g : 𝕜 → 𝕜'} (x : 𝕜) (hf : f x ≠ 0) (hg : g x ≠ 0) (hdf : DifferentiableAt 𝕜 f x)
(hdg : DifferentiableAt 𝕜 g x) : logDeriv (fun z => f z / g z) x = logDeriv f x - logDeriv g x := by
simp [field, logDeriv_apply, *]
