mathlib

ba627bc7 - feat(measure_theory/function/conditional_expectation): induction over Lp functions which are strongly measurable wrt a sub-sigma-algebra (#13129)

feat(measure_theory/function/conditional_expectation): induction over Lp functions which are strongly measurable wrt a sub-sigma-algebra (#13129) Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>