Commit 2022-07-26 16:40 86f80202

feat(measure_theory/function/conditional_expectation): pull-out property of the conditional expectation (#15274) We prove this result:

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.