Theorem MeasureTheory.condExp_of_not_integrable

Modification history

2025-01-26 17:26
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat: `μ[ofNat n * f|m] =ᵐ[μ] ofNat n * μ[f|m]` (#21001) …
Added MeasureTheory.condExp_of_not_integrableView on Github →