log — Mathlib

English

If fa is analytic within a set and f is positive on that set, then log∘f is analytic within that set.

Русский

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

LaTeX

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

Lean4

theorem log (fa : AnalyticWithinAt ℝ f s x) (m : 0 < f x) : AnalyticWithinAt ℝ (fun z ↦ Real.log (f z)) s x :=
  (analyticAt_log m).comp_analyticWithinAt fa

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