English
Conditional expectation in L2 is linear in its argument when combining indicator-based inputs; specifically, condExpIndSMul(hm, hs, hμs, x+y) equals the sum of condExpIndSMul(hm, hs, hμs, x) and condExpIndSMul(hm, hs, hμs, y).
Русский
Условное ожидание в L2 линейно по аргументу: condExpIndSMul(hm, hs, hμs, x+y) равно сумма condExpIndSMul(hm, hs, hμs, x) и condExpIndSMul(hm, hs, hμs, y).
LaTeX
$$$\operatorname{condExpIndSMul}(hm, hs, hμs, x+y) = \operatorname{condExpIndSMul}(hm, hs, hμs, x) + \operatorname{condExpIndSMul}(hm, hs, hμs, y).$$$
Lean4
theorem aestronglyMeasurable_condExpIndSMul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
AEStronglyMeasurable[m] (condExpIndSMul hm hs hμs x) μ :=
by
have h : AEStronglyMeasurable[m] (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) μ :=
aestronglyMeasurable_condExpL2 _ _
rw [condExpIndSMul]
exact ((toSpanSingleton ℝ x).continuous.comp_aestronglyMeasurable h).congr (coeFn_compLpL _ _).symm
