logDeriv_const — Mathlib

English

logDeriv of a product f·g equals logDeriv f plus logDeriv g, under nonzero evaluation and differentiability at x.

Русский

Логарифмическая производная произведения равна сумме логарифмических производных, при условии ненулевых значений и дифференцируемости в точке x.

LaTeX

$$$\forall f,g:\,\mathbb{K}\to\mathbb{K}',\; x: \mathbb{K},\; f(x)\neq 0,\; g(x)\neq 0,\; \text{DifferentiableAt } f x,\; \text{DifferentiableAt } g x\Rightarrow \logDeriv\,(f\cdot g) x = \logDeriv f x + \logDeriv g x$$$

Lean4

@[simp]
theorem logDeriv_const (a : 𝕜') : logDeriv (fun _ : 𝕜 ↦ a) = 0 :=
  by
  ext
  simp [logDeriv_apply]

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