Theorem MeasureTheory.set_integral_condexpInd

Modification history

2024-04-18 02:39

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

chore: replace `set_integral` with `setIntegral` (#12215) …

Deleted MeasureTheory.set_integral_condexpInd View on Github →

2023-06-17 11:16

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

feat: port MeasureTheory.Function.ConditionalExpectation.CondexpL1 (#5174)

Added MeasureTheory.set_integral_condexpInd View on Github →