integrable_of_nnreal — Mathlib

English

If a bounded continuous function f: X → NNReal is given on a space with a finite measure and opens measurable structure, then the real-valued composition NNReal.toReal ∘ f is integrable.

Русский

Если дана ограниченная непрерывная функция f: X → NNReal на пространстве с конечной мерой и открыто-измеримой структурой, то композиция NNReal.toReal ∘ f интегрируема.

LaTeX

$$$$\\text{Integrable}(\\,\\text{NNReal.toReal} \\circ f\\,).$$$$

Lean4

theorem integrable_of_nnreal [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) : Integrable (((↑) : ℝ≥0 → ℝ) ∘ ⇑f) μ :=
  by
  refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩
  simp only [hasFiniteIntegral_iff_enorm, Function.comp_apply, NNReal.enorm_eq]
  exact lintegral_lt_top_of_nnreal _ f

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