English
For f: α → ℝ, the eLpNorm of μ[f|m] is bounded by the eLpNorm of f with respect to μ for p = 1.
Русский
Для f: α → ℝ нормa eLp по μ[ f|m ] не превышает норму eLp f по μ при p = 1.
LaTeX
$$$$ eLpNorm(\\mu[f|m], 1, \\mu) \\leq eLpNorm(f, 1, \\mu). $$$$
Lean4
theorem eLpNorm_one_condExp_le_eLpNorm (f : α → ℝ) : eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ :=
by
by_cases hf : Integrable f μ
swap; · rw [condExp_of_not_integrable hf, eLpNorm_zero]; exact zero_le _
by_cases hm : m ≤ m0
swap; · rw [condExp_of_not_le hm, eLpNorm_zero]; exact zero_le _
by_cases hsig : SigmaFinite (μ.trim hm)
swap; · rw [condExp_of_not_sigmaFinite hm hsig, eLpNorm_zero]; exact zero_le _
calc
eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm (μ[(|f|)|m]) 1 μ :=
by
refine eLpNorm_mono_ae ?_
filter_upwards [condExp_mono hf hf.abs (ae_of_all μ (fun x => le_abs_self (f x) : ∀ x, f x ≤ |f x|)),
(condExp_neg ..).symm.le.trans
(condExp_mono hf.neg hf.abs (ae_of_all μ (fun x => neg_le_abs (f x) : ∀ x, -f x ≤ |f x|)))] with
x hx₁ hx₂
exact abs_le_abs hx₁ hx₂
_ = eLpNorm f 1 μ :=
by
rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm, ←
ENNReal.toReal_eq_toReal (hasFiniteIntegral_iff_enorm.mp integrable_condExp.2).ne
(hasFiniteIntegral_iff_enorm.mp hf.2).ne,
← integral_norm_eq_lintegral_enorm (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable, ←
integral_norm_eq_lintegral_enorm hf.1]
simp_rw [Real.norm_eq_abs]
rw (config := { occs := .pos [2] }) [← integral_condExp hm]
refine integral_congr_ae ?_
have : 0 ≤ᵐ[μ] μ[(|f|)|m] := by
rw [← condExp_zero]
exact condExp_mono (integrable_zero _ _ _) hf.abs (ae_of_all μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))
filter_upwards [this] with x hx
exact abs_eq_self.2 hx
