clog — Mathlib

English

If f is analytic on a set and f(z) avoids the slit for all z in the set, then log(f) is analytic on the set.

Русский

Если f аналитична на множестве и для всех z в множестве f(z) избегает разрез, то log(f) аналитична на множестве.

LaTeX

$$$\\text{AnalyticOn}(\\log \\circ f, s)$ provided $f(z)\\in\\text{slitPlane}$ for all z∈s and f analytic on s$$

Lean4

/-- `log` is analytic away from nonpositive reals -/
theorem clog (fs : AnalyticOnNhd ℂ f s) (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOnNhd ℂ (fun z ↦ log (f z)) s :=
  fun z n ↦ (analyticAt_clog (m z n)).comp (fs z n)

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