English
For measurable set s with finite μ-measure, the conditional expectation in L2 of the indicator-smul construction is a well-defined Lp object, yielding a Bochner-valued function that is integrable.
Русский
Для измеримого множества s с конечной мерой μ, условное ожидание в L2 конструктции indicator-smul является корректным объектом Lp, образующим Bochner-значную функцию, которая интегрируема.
LaTeX
$$$\forall s\ (hs : MeasurableSet s) (hμs : μ s \neq ∞)\, (x : G),\; Integrable\big( \operatorname{condExpIndSMul}(hm, hs, hμs, x) \big)_{μ}. $$$
Lean4
/-- Conditional expectation of the indicator of a measurable set with finite measure, in L2. -/
noncomputable def condExpIndSMul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) : Lp G 2 μ :=
(toSpanSingleton ℝ x).compLpL 2 μ (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs (1 : ℝ)))
