English
For a simple function f and integrable g, the conditional expectation of f · g equals f times the CondExp of g, a.e.
Русский
Для простой функции f и интегрируемой g CondExp(f·g) = f·CondExp(g) почти везде.
LaTeX
$$$$ \\mu[ f\\cdot g|m ] =_{a.e.} f \\cdot \\mu[g|m], $$$$
Lean4
/-- Auxiliary lemma for `condExp_mul_of_stronglyMeasurable_left`. -/
theorem condExp_stronglyMeasurable_simpleFunc_mul (hm : m ≤ m0) (f : @SimpleFunc α m ℝ) {g : α → ℝ}
(hg : Integrable g μ) : μ[(f * g : α → ℝ)|m] =ᵐ[μ] f * μ[g|m] :=
by
have : ∀ (s c) (f : α → ℝ), Set.indicator s (Function.const α c) * f = s.indicator (c • f) :=
by
intro s c f
ext1 x
by_cases hx : x ∈ s
· simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul, Function.const_apply]
· simp only [hx, Pi.mul_apply, Set.indicator_of_notMem, not_false_iff, zero_mul]
apply @SimpleFunc.induction _ _ m _ (fun f => _) (fun c s hs => ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ => ?_) f
· simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
Set.piecewise_eq_indicator]
rw [this, this]
refine (condExp_indicator (hg.smul c) hs).trans ?_
filter_upwards [condExp_smul c g m] with x hx
classical simp_rw [Set.indicator_apply, hx]
· have h_add := @SimpleFunc.coe_add _ _ m _ g₁ g₂
calc
μ[⇑(g₁ + g₂) * g|m] =ᵐ[μ] μ[⇑g₁ * g|m] + μ[⇑g₂ * g|m] := by rw [h_add, add_mul];
exact condExp_add (hg.simpleFunc_mul' hm _) (hg.simpleFunc_mul' hm _) _
_ =ᵐ[μ] ⇑g₁ * μ[g|m] + ⇑g₂ * μ[g|m] := (EventuallyEq.add h_eq₁ h_eq₂)
_ =ᵐ[μ] ⇑(g₁ + g₂) * μ[g|m] := by rw [h_add, add_mul]
