lintegral_trim_ae — Mathlib

English

For hm: m ≤ m0 and Measurable f (with respect to the subspace m), the lintegral with respect to μ.trim hm equals the lintegral with respect to μ.

Русский

Пусть hm: m ≤ m0 и f измерима относительно m; интеграл по обрезанной мере μ.trim hm равен интегралу по μ.

LaTeX

$$$\forall hm : MeasurableSpace.instLE.le m m0, \; \forall f : α \to \mathbb{R}_{\ge 0}^{\infty}, \; \mathrm{Measurable}[m] f \Rightarrow ∫^- a, f a ∂(μ.trim hm) = ∫^- a, f a ∂μ$$$

Lean4

theorem lintegral_trim_ae {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : AEMeasurable f (μ.trim hm)) :
    ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ := by
  rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
    lintegral_trim hm hf.measurable_mk]

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