norm_integral_le_integral_norm — Mathlib

English

If ‖f(x)‖ ≤ C almost everywhere, then ‖∫ f dμ‖ ≤ C μ(univ).

Русский

Если почти всюду выполняется ‖f(x)‖ ≤ C, то ‖∫ f dμ‖ ≤ C μ(весь мир).

LaTeX

$$$\\\\|\\\\int x \\, f(x) \\\\| \\\\leq C \\\\cdot μ(\\\\text{univ})$$$

Lean4

theorem norm_integral_le_integral_norm (f : α → G) : ‖∫ a, f a ∂μ‖ ≤ ∫ a, ‖f a‖ ∂μ :=
  by
  have le_ae : ∀ᵐ a ∂μ, 0 ≤ ‖f a‖ := Eventually.of_forall fun a => norm_nonneg _
  by_cases h : AEStronglyMeasurable f μ
  ·
    calc
      ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) := norm_integral_le_lintegral_norm _
      _ = ∫ a, ‖f a‖ ∂μ := (integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm
  · rw [integral_non_aestronglyMeasurable h, norm_zero]
    exact integral_nonneg_of_ae le_ae

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