clog — Mathlib

English

Log is analytic away from nonpositive reals, so composing with a function avoiding the slit yields analytic log∘f.

Русский

Логарифм аналитичен вне неположительных вещественных, поэтому композиция с функцией, не попадающей в разрез, даёт аналитичность log∘f.

LaTeX

$$$\\text{AnalyticAt}(\\mathbb{C}, \\log \\circ f, x)$ under the condition $f(x)\\in\\text{slitPlane}$ and $f$ analytic at x$$

Lean4

/-- `log` is analytic away from nonpositive reals -/
@[fun_prop]
theorem clog (fa : AnalyticAt ℂ f x) (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ log (f z)) x :=
  (analyticAt_clog m).comp fa

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