eLpNorm_condExp_le — Mathlib

English

The eLp norm of the conditional expectation is bounded by the eLp norm of the original function.

Русский

eLp-норма условного ожидания не превышает eLp-норму исходной функции.

LaTeX

$$$eLpNorm(\\mu[f|m],\, 2, \\mu) \\le eLpNorm(f, 2, \\mu)$$$

Lean4

theorem eLpNorm_condExp_le : eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ :=
  by
  by_cases hm : m ≤ m₀; swap
  · simp [condExp_of_not_le hm]
  by_cases hfμ : SigmaFinite (μ.trim hm); swap
  · rw [condExp_of_not_sigmaFinite hm hfμ]
    simp
  by_cases hfi : Integrable f μ; swap
  · rw [condExp_of_not_integrable hfi]
    simp
  obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞
  · simp [hf]
  replace hf : MemLp f 2 μ := ⟨hfi.1, Ne.lt_top' fun a ↦ hf a.symm⟩
  rw [← eLpNorm_congr_ae (hf.condExpL2_ae_eq_condExp' (𝕜 := ℝ) hm hfi)]
  refine le_trans (eLpNorm_condExpL2_le hm _) ?_
  rw [eLpNorm_congr_ae hf.coeFn_toLp]

Похожие утверждения