English
On a measurable set s, the integral of the absolute value of μ[f|m] is bounded by the integral of |f|.
Русский
На измеримом множестве s интеграл по |μ[f|m]| не больше интеграла по |f|.
LaTeX
$$$$ \\int_{s} |(\\mu[f|m])(x)| \\, d\\mu(x) \\leq \\int_{s} |f(x)| \\, d\\mu(x). $$$$
Lean4
theorem setIntegral_abs_condExp_le {s : Set α} (hs : MeasurableSet[m] s) (f : α → ℝ) :
∫ x in s, |(μ[f|m]) x| ∂μ ≤ ∫ x in s, |f x| ∂μ :=
by
by_cases hnm : m ≤ m0
swap
· simp_rw [condExp_of_not_le hnm, 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
have : ∫ x in s, |(μ[f|m]) x| ∂μ = ∫ x, |(μ[s.indicator f|m]) x| ∂μ :=
by
rw [← integral_indicator (hnm _ hs)]
refine integral_congr_ae ?_
have : (fun x => |(μ[s.indicator f|m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f|m]) x| :=
(condExp_indicator hfint hs).fun_comp abs
refine EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm
rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
simp only [Real.norm_eq_abs]
rw [this, ← integral_indicator (hnm _ hs)]
refine (integral_abs_condExp_le _).trans (le_of_eq <| integral_congr_ae <| Eventually.of_forall fun x => ?_)
simp_rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
