English
For hm ≤ m0 and f ∈ Lp E' 2 μ, and hs measurable, the integral over a measurable set s of condExpL2 equals the integral of f over s.
Русский
Пусть hm ≤ m0 и f ∈ Lp E' 2 μ, и hs измеримо; то интеграл по измеримому множеству s кондExpL2 от f равен интегралу f по s.
LaTeX
$$$\int_{x \in s} (\operatorname{condExpL2} E' 𝕜 hm f : α \to E')\, dμ = \int_{x \in s} f(x) \, dμ$$$
Lean4
/-- `condExpL2` verifies the equality of integrals defining the conditional expectation. -/
theorem integral_condExpL2_eq (hm : m ≤ m0) (f : Lp E' 2 μ) (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) :
∫ x in s, (condExpL2 E' 𝕜 hm f : α → E') x ∂μ = ∫ x in s, f x ∂μ :=
by
rw [← sub_eq_zero, ←
integral_sub' (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs)
(integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs)]
refine integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_
· rw [integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub (↑(condExpL2 E' 𝕜 hm f)) f).symm)]
exact integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs
intro c
simp_rw [Pi.sub_apply, inner_sub_right]
rw [integral_sub ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)
((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)]
have h_ae_eq_f := MemLp.coeFn_toLp (E := 𝕜) ((Lp.memLp f).const_inner c)
rw [sub_eq_zero, ← setIntegral_congr_ae (hm s hs) ((condExpL2_const_inner hm f c).mono fun x hx _ => hx), ←
setIntegral_congr_ae (hm s hs) (h_ae_eq_f.mono fun x hx _ => hx)]
exact integral_condExpL2_eq_of_fin_meas_real _ hs hμs
