Conditional expectation of product

Stream: Is there code for X?

[Yaël Dillies]

I'm trying to prove that if g is m-measurable then μ[f * g | m] =ᵐ[μ] μ[f | m] * g. I thought it would be generalisable to μ[fun ω ↦ L ω (f ω)] =ᵐ[μ] fun ω ↦ L ω (μ[f | m] ω) where L is a m-measurable random linear map. Is this anywhere?

[Yaël Dillies]

Here is my attempt:

import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

namespace MeasureTheory
variable {Ω R E F : Type*}
  {m m₀ : MeasurableSpace Ω} {μ : Measure Ω} {s : Set Ω}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]

/-- For `L` a `m`-measurable random linear map and `X` a random variable, the expectation of `L(X)`
conditional to `m` is `L` applied to the expectation of `X` conditional to `m`. -/
lemma condexp_continuousLinearMap_of_stronglyMeasurable (L : Ω → (E →L[ℝ] F))
    (hL : ∀ x, StronglyMeasurable[m] (L · x)) (f : Ω → E) :
    μ[fun ω ↦ L ω (f ω) | m] =ᵐ[μ] fun ω ↦ L ω ((μ[f | m]) ω) := by
  by_cases hm : m ≤ m₀; swap
  · simp [condexp_of_not_le hm, Pi.zero_def]
  by_cases hμm : SigmaFinite (μ.trim hm); swap
  · simp [condexp_of_not_sigmaFinite hm hμm, Pi.zero_def]
  haveI : SigmaFinite (μ.trim hm) := hμm
  refine (condexp_ae_eq_condexpL1 hm _).trans ?_
  sorry
  -- Taken from the end of the proof of `condexp_smul`
  -- rw [condexpL1_smul c f]
  -- refine (@condexp_ae_eq_condexpL1 _ _ _ _ _ m _ _ hm _ f).mp ?_
  -- refine (coeFn_smul c (condexpL1 hm μ f)).mono fun x hx1 hx2 => ?_
  -- simp only [hx1, hx2, Pi.smul_apply]

section NormedRing
variable
  [NormedRing R] [NormedSpace ℝ R] [CompleteSpace R] [IsScalarTower ℝ R R] [SMulCommClass ℝ R R]
  {f g : Ω → R}

lemma condexp_mul_of_stronglyMeasurable_left (hf : StronglyMeasurable[m] f) (g : Ω → R) :
    μ[f * g | m] =ᵐ[μ] f * μ[g | m] :=
  condexp_continuousLinearMap_of_stronglyMeasurable
    (fun ω ↦ ContinuousLinearMap.mul _ _ (f ω)) hf.mul_const _

lemma condexp_mul_of_stronglyMeasurable_right (hg : StronglyMeasurable[m] g) (f : Ω → R) :
    μ[f * g | m] =ᵐ[μ] μ[f | m] * g :=
  condexp_continuousLinearMap_of_stronglyMeasurable
    (fun ω ↦ (ContinuousLinearMap.mul _ _).flip (g ω)) hg.const_mul _

end NormedRing

[Rémy Degenne]

We have this result, that looks related: MeasureTheory.condexp_stronglyMeasurable_mul

And line 221 of that file, there is the following todo:
-- TODO: this section could be generalized beyond multiplication, to any bounded bilinear map.

[Rémy Degenne]

But at that moment I had no use for the generalization so I did not do it.
See Hytönen et al., Analysis in Banach Spaces (vol. 1), proposition 2.6.31

[Yaël Dillies]

That's enough for my use case (proving the law of total variance), thanks!

[Rémy Degenne]

Note that the book uses sigma-integrability, which makes proofs a bit more complicated. We defined the conditional expectation only for integrable functions, so the proof can be simplified slightly.