Theorem MeasureTheory.condExp_of_not_integrable

Modification history

2026-01-26 14:38

Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

style: consistently put whitespace around pipes in conditional expectation and variance (#33815) …

Modified MeasureTheory.condExp_of_not_integrable View on Github →

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_integrable View on Github →