Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.rn_deriv_ae_eq_condexp

Modification history

2022-08-09 17:00
src/measure_theory/function/conditional_expectation/basic.lean
chore(measure_theory/function/condexp): split `conditional_expectation` into multiple files (#15714)
Modified measure_theory.rn_deriv_ae_eq_condexpView on Github →
2022-05-11 18:53
src/measure_theory/function/conditional_expectation.lean
chore(measure_theory/function/conditional_expectation): change the definition of condexp and its notation (#14010) …
Modified measure_theory.rn_deriv_ae_eq_condexpView on Github →
2021-10-01 20:35
src/measure_theory/function/conditional_expectation.lean
feat(measure_theory/function/conditional_expectation): conditional expectation on real functions equal Radon-Nikodym derivative (#9378)
Added measure_theory.rn_deriv_ae_eq_condexpView on Github →