Theorem MeasureTheory.integral_condexp

Modification history

2025-01-22 13:49

Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

chore: rename `condexp` to `condExp` (#20930) …

Deleted MeasureTheory.integral_condexp View on Github →

2024-06-22 12:48

Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

feat(MeasureTheory/Function/ConditionalExpectation): relax `integral_condexp` assumption and add `integral_condexp_indicator` (#13932) …

Modified MeasureTheory.integral_condexp View on Github →

2023-06-17 12:30

Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

feat: port MeasureTheory.Function.ConditionalExpectation.Basic (#4898)

Added MeasureTheory.integral_condexp View on Github →