mathlib

86f80202 - feat(measure_theory/function/conditional_expectation): pull-out property of the conditional expectation (#15274)

feat(measure_theory/function/conditional_expectation): pull-out property of the conditional expectation (#15274) We prove this result: ```lean lemma condexp_strongly_measurable_mul {f g : α → ℝ} (hf : strongly_measurable[m] f) (hfg : integrable (f * g) μ) (hg : integrable g μ) : μ[f * g | m] =ᵐ[μ] f * μ[g | m] := ``` This could be extended beyond multiplication, to any bounded bilinear map, but we leave this to a future PR. For now we only prove the real multiplication case, which is needed for #14909 and #14933.