Commit 2021-12-09 09:57 e3d9adf1

View on Github →

chore(measure_theory/function/conditional_expectation): change condexp notation (#10584) The previous definition and notation showed the measurable_space argument only through the other argument m \le m0, which tends to be replaced by _ in the goal view if it becomes complicated.

Estimated changes

Modified src/measure_theory/function/conditional_expectation.lean

modified theorem measure_theory.condexp_ae_eq_condexp_L1

modified theorem measure_theory.condexp_const

modified theorem measure_theory.condexp_neg

modified theorem measure_theory.condexp_smul

modified theorem measure_theory.condexp_undef

modified theorem measure_theory.condexp_zero

modified theorem measure_theory.integrable_condexp

modified theorem measure_theory.integral_condexp

modified theorem measure_theory.measurable_condexp

Modified src/probability_theory/notation.lean