hasDerivAt_log

Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

URI: https://scilib.ai/kg/mathlib#Complex.hasDerivAt_log

English

For x in the slit plane, the (complex) derivative of log at x is 1/x.

Русский

Для x на разрезанной плоскости производная log в точке x равна 1/x.

LaTeX

$$$$ \frac{d}{dz}\log z \Big|_{z=x} = \frac{1}{x}, \quad x \in \mathrm{slitPlane}. $$$$

Lean4

theorem hasDerivAt_log {z : ℂ} (hz : z ∈ slitPlane) : HasDerivAt log z⁻¹ z :=
  HasStrictDerivAt.hasDerivAt <| hasStrictDerivAt_log hz

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru