Commit 2022-05-11 18:53 0302cfdd

chore(measure_theory/function/conditional_expectation): change the definition of condexp and its notation (#14010) Before this PR, the conditional expectation condexp was defined using an argument (hm : m ≤ m0). This changes the definition to take only m, and assigns the default value 0 if we don't have m ≤ m0. The notation for condexp m μ f is simplified to μ[f|m]. The change makes the proofs of the condexp API longer, but no change is needed to lemmas outside of that file. See the file martingale.lean: the notation is now simpler, but otherwise little else changes besides removing the now unused argument [sigma_finite_filtration μ ℱ] from many lemmas. Also add an instance is_finite_measure.sigma_finite_filtration: we had a lemma with both is_finite_measure and sigma_finite_filtration arguments, but the first one implies the other.