mathlib

0302cfdd - chore(measure_theory/function/conditional_expectation): change the definition of condexp and its notation (#14010)

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.