log — Mathlib

English

The real logarithm is interval-integrable (with respect to volume) on intervals not containing zero.

Русский

Логарифм по Лебегу интегрируем на интервалах, не содержащих ноль.

LaTeX

$$$\text{IntervalIntegrable } \log(x) \text{ на интервале без 0}$$$

Lean4

@[simp]
theorem _root_.IntervalIntegrable.log (hf : ContinuousOn f [[a, b]]) (h : ∀ x : ℝ, x ∈ [[a, b]] → f x ≠ 0) :
    IntervalIntegrable (fun x => log (f x)) μ a b :=
  (ContinuousOn.log hf h).intervalIntegrable

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