log — Mathlib

English

If f is analytic on s and f is positive on s, then log∘f is analytic on s.

Русский

Если f аналитична на s и положительна на s, то log∘f аналитична на s.

LaTeX

$$$\\text{AnalyticOn}_\\mathbb{R}(\\log\\circ f)s\\;\\text{from } \\text{AnalyticOn}_\\mathbb{R} f s$ with $\\forall x\\in s, f(x)>0$.$$

Lean4

theorem log (fs : AnalyticOnNhd ℝ f s) (m : ∀ x ∈ s, 0 < f x) : AnalyticOnNhd ℝ (fun z ↦ Real.log (f z)) s := fun z n ↦
  (analyticAt_log (m z n)).comp (fs z n)

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