Theorems · Theorem · measure theory

MeasureTheory.condLExp_enorm

∀ {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → ℝ},
  MeasureTheory.Integrable f μ → 0 ≤ᵐ[μ] f → μ⁻[fun x => ‖f x‖ₑ | m] =ᵐ[μ] fun x => ‖μ[f | m] x‖ₑ

The two definitions of the conditional expectation condExp and condLExp (for Bochner and Lebesgue integrals respectively) agree almost everywhere.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Cited by

1 results in Mathlib

Foundations

Depth 301 from the axioms · uses propext, Classical.choice, Quot.sound