English
With hs measurable and finite μ(s), the L2 conditional expectation of the indicator yields a bound in the real-valued setting.
Русский
При hs измеримо и μ(s) конечно, линтеграл по t для condExpL2(indicatorConstLp 2 hs hμs 1) ≤ μ(s ∩ t).
LaTeX
$$$\int_{a \in t} \| (\operatorname{condExpL2} E' \ 𝕜 \; hm \; (\operatorname{indicatorConstLp} 2 hs hμs 1) : α \to_2[μ] \mathbb{R}) (a) \|_+ \, dμ(a) \le μ(s \cap t) $$$
Lean4
theorem lintegral_nnnorm_condExpL2_indicator_le_real (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (ht : MeasurableSet[m] t)
(hμt : μ t ≠ ∞) : ∫⁻ a in t, ‖(condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) a‖₊ ∂μ ≤ μ (s ∩ t) :=
by
refine (lintegral_nnnorm_condExpL2_le ht hμt _).trans (le_of_eq ?_)
have h_eq :
∫⁻ x in t, ‖(indicatorConstLp 2 hs hμs (1 : ℝ)) x‖₊ ∂μ = ∫⁻ x in t, s.indicator (fun _ => (1 : ℝ≥0∞)) x ∂μ :=
by
refine lintegral_congr_ae (ae_restrict_of_ae ?_)
refine (@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_
dsimp only
rw [hx]
classical
simp_rw [Set.indicator_apply]
split_ifs <;> simp
rw [h_eq, lintegral_indicator hs, lintegral_const, Measure.restrict_restrict hs]
simp only [one_mul, Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply]
