English
The L1-norm of μ[f|m] is bounded by the L1-norm of f, i.e., the conditional expectation is a contraction on L1.
Русский
План в L1: ||μ[f|m]||_1 ≤ ||f||_1, то есть CondExp сужает L1-норму.
LaTeX
$$$$ \\int |(\\mu[f|m])(x)| \\, d\\mu(x) \\leq \\int |f(x)| \\, d\\mu(x). $$$$
Lean4
theorem integral_abs_condExp_le (f : α → ℝ) : ∫ x, |(μ[f|m]) x| ∂μ ≤ ∫ x, |f x| ∂μ :=
by
by_cases hm : m ≤ m0
swap
· simp_rw [condExp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero]
positivity
by_cases hfint : Integrable f μ
swap
· simp only [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero, integral_const, Algebra.id.smul_eq_mul,
mul_zero]
positivity
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
· apply ENNReal.toReal_mono <;> simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_enorm]
· exact hfint.2.ne
· rw [← eLpNorm_one_eq_lintegral_enorm, ← eLpNorm_one_eq_lintegral_enorm]
exact eLpNorm_one_condExp_le_eLpNorm _
· filter_upwards with x using abs_nonneg _
· simp_rw [← Real.norm_eq_abs]
exact hfint.1.norm
· filter_upwards with x using abs_nonneg _
· simp_rw [← Real.norm_eq_abs]
exact (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable.norm
