hasStrictFDerivAt_log_real — Mathlib

English

For x in the slit plane, the Fréchet derivative of log at x is the real-linear map v ↦ (v/x).

Русский

Для x на области разреза производная log по Фреше равна линейному отображению v ↦ v/x (относительно вещественной линейности).

LaTeX

$$$$ \text{The Frechet derivative of } \log \text{ at } x \in \mathrm{slitPlane} \text{ is } v \mapsto x^{-1} v. $$$$

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_log_real {x : ℂ} (h : x ∈ slitPlane) : HasStrictFDerivAt log (x⁻¹ • (1 : ℂ →L[ℝ] ℂ)) x :=
  (hasStrictDerivAt_log h).complexToReal_fderiv

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