English
Pull-out property: if f is strongly measurable and g is integrable, then CondExp of f·g equals f times CondExp g (left case).
Русский
Свойство выноса: если f сильно измеримо, а g интегрируемо, CondExp(f·g) = f·CondExp(g) слева.
LaTeX
$$$$ \\mu[ f \\cdot g|m ] =_{a.e.} f \\cdot \\mu[g|m], $$$$
Lean4
/-- Pull-out property of the conditional expectation. -/
theorem condExp_mul_of_stronglyMeasurable_left {f g : α → ℝ} (hf : StronglyMeasurable[m] f) (hfg : Integrable (f * g) μ)
(hg : Integrable g μ) : μ[f * g|m] =ᵐ[μ] f * μ[g|m] :=
by
by_cases hm : m ≤ m0; swap; · simp_rw [condExp_of_not_le hm]; rw [mul_zero]
by_cases hμm : SigmaFinite (μ.trim hm)
swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; rw [mul_zero]
haveI : SigmaFinite (μ.trim hm) := hμm
obtain ⟨sets, sets_prop, h_univ⟩ := hf.exists_spanning_measurableSet_norm_le hm μ
simp_rw [forall_and] at sets_prop
obtain ⟨h_meas, h_finite, h_norm⟩ := sets_prop
suffices ∀ n, ∀ᵐ x ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x
by
rw [← ae_all_iff] at this
filter_upwards [this] with x hx
obtain ⟨i, hi⟩ : ∃ i, x ∈ sets i :=
by
have h_mem : x ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
simpa using h_mem
exact hx i hi
refine fun n => ae_imp_of_ae_restrict ?_
suffices (μ.restrict (sets n))[f * g|m] =ᵐ[μ.restrict (sets n)] f * (μ.restrict (sets n))[g|m]
by
refine (condExp_restrict_ae_eq_restrict hm (h_meas n) hfg).symm.trans ?_
exact this.trans (EventuallyEq.rfl.mul (condExp_restrict_ae_eq_restrict hm (h_meas n) hg))
suffices
(μ.restrict (sets n))[(sets n).indicator f * g|m] =ᵐ[μ.restrict (sets n)]
(sets n).indicator f * (μ.restrict (sets n))[g|m]
by
refine EventuallyEq.trans ?_ (this.trans ?_)
· exact condExp_congr_ae ((indicator_ae_eq_restrict <| hm _ <| h_meas n).symm.mul EventuallyEq.rfl)
· exact (indicator_ae_eq_restrict <| hm _ <| h_meas n).mul EventuallyEq.rfl
have : IsFiniteMeasure (μ.restrict (sets n)) := by
constructor
rw [Measure.restrict_apply_univ]
exact h_finite n
refine condExp_stronglyMeasurable_mul_of_bound hm (hf.indicator (h_meas n)) hg.integrableOn n ?_
filter_upwards with x
by_cases hxs : x ∈ sets n
· simpa only [hxs, Set.indicator_of_mem] using h_norm n x hxs
· simp only [hxs, Set.indicator_of_notMem, not_false_iff, _root_.norm_zero, Nat.cast_nonneg]