English
Let μ trim hm be sigma-finite and s be a measurable set with μ s ≠ ∞. Then for every x in the target space E', the L2 conditional expectation of the function obtained by multiplying x on s (and 0 outside) is integrable with respect to μ.
Русский
Пусть μ.trim hm является σ-конечным, s — измеримое множество с μ s ≠ ∞. Тогда для каждого x ∈ E' интегрируемость по мере μ выполняется для условного ожидания в L2 функции, заданной умножением x на s (и нулём вне s).
LaTeX
$$$\forall\text{(hm : m ≤ m0)}, [\Sigma\text{Finite}(μ.trim hm)], \text{MeasurableSet}(s), μ s \neq \infty, x \in E':\; \text{Integrable}_{μ}\Big( \operatorname{condExpL2} \big( E', 𝕜, hm, \operatorname{indicatorConstLp}(2, hs, hμs, x) \big) \Big).$$$
Lean4
/-- If the measure `μ.trim hm` is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable. -/
theorem integrable_condExpL2_indicator (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
(x : E') : Integrable (ε := E') (condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x)) μ :=
by
refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊) (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_
· exact Lp.aestronglyMeasurable _
· refine fun t ht hμt => (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_
gcongr
apply Set.inter_subset_left
