log — Mathlib

English

If f is analytic on a real interval, and f is positive there, then Real.log∘f is analytic on that interval.

Русский

Если f аналитична на действительном интервале и там положительна, то Real.log∘f аналитична на этом интервале.

LaTeX

$$$\\text{AnalyticOn}_\\mathbb{R}(\\log\\circ f)\\text{ on } s$ given $\\text{AnalyticOn}_\\mathbb{R} f s$ and $\\forall x\\in s, f(x)>0$.$$

Lean4

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

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