English
Let μ be a measure and hm ≤ m0 be measurable spaces on α. Suppose s and t are measurable with μ(s) ≠ ∞ and μ(t) ≠ ∞, and x belongs to G'. Then the integral over s of the conditional expectation condExpIndSMul hm ht hμt applied to x equals the real-measure μ.real(t ∩ s) times x.
Русский
Пусть μ — мера на α, hm ≤ m0 — измеримые пространства на α. Пусть s и t измеримы и μ(s), μ(t) конечны, и x ∈ G'. Тогда интеграл по s от condExpIndSMul hm ht hμt( x ) равен μ.real(t ∩ s)·x.
LaTeX
$$$$\\displaystyle \\int_{s} (\\operatorname{condExpIndSMul}_{hm ht hμt} x)(a)\\, d\\mu(a) \\\\ = \\mu_{\\mathbb{R}}(t \\cap s)\\, x.$$$$
Lean4
theorem setIntegral_condExpIndSMul (hs : MeasurableSet[m] s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞)
(x : G') : ∫ a in s, (condExpIndSMul hm ht hμt x) a ∂μ = μ.real (t ∩ s) • x :=
calc
∫ a in s, (condExpIndSMul hm ht hμt x) a ∂μ =
∫ a in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) a • x ∂μ :=
setIntegral_congr_ae (hm s hs) ((condExpIndSMul_ae_eq_smul hm ht hμt x).mono fun _ hx _ => hx)
_ = (∫ a in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) a ∂μ) • x := (integral_smul_const _ x)
_ = μ.real (t ∩ s) • x := by rw [setIntegral_condExpL2_indicator hs ht hμs hμt]
