analyticOn_log — Mathlib

English

If a real-valued function f is analytic on a set, and f is positive on that set, then log∘f is analytic on that set.

Русский

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

LaTeX

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

Lean4

theorem analyticOn_log : AnalyticOn ℝ Real.log (Set.Ioi 0) :=
  analyticOnNhd_log.analyticOn

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