English
Integrating condExpL2 of an indicator-like function over s yields the real measure of t ∩ s.
Русский
Интегрирование condExpL2 от индикаторной функции по s даёт действительную меру пересечения t и s.
LaTeX
$$$\int x in s, (condExpL2 E 𝕜 hm (indicatorConstLp 2 ht hμt 1) : α → \mathbb{R}) x ∂μ = μ.real (t \cap s)$$$
Lean4
/-- If the measure `μ.trim hm` is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable. -/
theorem integrable_condExpIndSMul (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
(x : G) : Integrable (condExpIndSMul hm 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_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_
gcongr
apply Set.inter_subset_left
