contDiffAt_log — Mathlib

English

On the slit plane, log is contDiff of all orders (indeed analytic).

Русский

На области разреза логарифм является гладким во всех порядках (на самом деле аналитичен).

LaTeX

$$$$ \forall z \in \mathrm{slitPlane},\; \mathrm{ContDiff}_{\mathbb{C}}^{\infty}(\log)(z). $$$$

Lean4

theorem contDiffAt_log {x : ℂ} (h : x ∈ slitPlane) {n : WithTop ℕ∞} : ContDiffAt ℂ n log x :=
  expPartialHomeomorph.contDiffAt_symm_deriv (exp_ne_zero <| log x) h (hasDerivAt_exp _) contDiff_exp.contDiffAt

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