toReal_lintegral_coe_eq_integral — Mathlib

English

For a bounded continuous f: X → NNReal, the real-valued lintegral of its Ennreal-coercion equals the real integral of f.

Русский

Для ограниченной непрерывной f: X → NNReal линегральный интеграл её Ennreal-переобразования равен реальному интегралу f.

LaTeX

$$$$\\left(\\int⁻ x, (f(x) : \\mathbb{R}_{\\ge 0}^{∞}) ∂μ\\right)^{toReal} = \\int x, (f(x) : \\mathbb{R}) ∂μ.$$$$

Lean4

theorem toReal_lintegral_coe_eq_integral [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) (μ : Measure X) :
    (∫⁻ x, (f x : ℝ≥0∞) ∂μ).toReal = ∫ x, (f x : ℝ) ∂μ :=
  by
  rw [integral_eq_lintegral_of_nonneg_ae _
      (by simpa [Function.comp_apply] using (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]
  · simp only [ENNReal.ofReal_coe_nnreal]
  · exact Eventually.of_forall (by simp only [Pi.zero_apply, NNReal.zero_le_coe, imp_true_iff])

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