English
Let hm ≤ m0, s be measurable and μ(s) ≠ ∞ with Sigma-finiteness of μ.trim hm. Then the conditional expectation condExpL2 of the indicator (with a unit value) is nonnegative almost everywhere.
Русский
Пусть hm ≤ m0, s измеримо и μ(s) ≠ ∞, причём μ.trim hm сигма-финитна. Тогда condExpL2 для индикатора (со значением 1) неотрицательно почти всюду.
LaTeX
$$$$ (0 \\leq_{\mu} \\mathrm{condExpL2}_{\\mathbb{R},\\mathbb{R}}(hm, \\mathbf{1}_s)) \\, a.e.$$$
Lean4
theorem condExpL2_indicator_nonneg (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) [SigmaFinite (μ.trim hm)] :
(0 : α → ℝ) ≤ᵐ[μ] condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) :=
by
have h : AEStronglyMeasurable[m] (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) μ :=
aestronglyMeasurable_condExpL2 _ _
refine EventuallyLE.trans_eq ?_ h.ae_eq_mk.symm
refine @ae_le_of_ae_le_trim _ _ _ _ _ _ hm (0 : α → ℝ) _ ?_
refine ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite ?_ ?_
· rintro t - -
refine @Integrable.integrableOn _ _ m _ _ _ _ _ ?_
refine Integrable.trim hm ?_ h.stronglyMeasurable_mk
rw [integrable_congr h.ae_eq_mk.symm]
exact integrable_condExpL2_indicator hm hs hμs _
· intro t ht hμt
rw [← setIntegral_trim hm h.stronglyMeasurable_mk ht]
have h_ae : ∀ᵐ x ∂μ, x ∈ t → h.mk _ x = (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) x := by
filter_upwards [h.ae_eq_mk] with x hx using fun _ => hx.symm
rw [setIntegral_congr_ae (hm t ht) h_ae, setIntegral_condExpL2_indicator ht hs ((le_trim hm).trans_lt hμt).ne hμs]
exact ENNReal.toReal_nonneg
