norm_integral_le_of_norm_le — Mathlib

English

If ‖f(x)‖ ≤ g(x) a.e. with g integrable, then ‖∫ f‖ ≤ ∫ g.

Русский

Если ‖f(x)‖ ≤ g(x) почти всюду и g интегрируема, то ‖∫ f‖ ≤ ∫ g.

LaTeX

$$$\\\\|\\\\int x \\, f(x) \\, d\\\\mu\\\\| \\\\leq \\\\int x \\, g(x) \\, d\\\\mu$$$

Lean4

theorem norm_integral_le_of_norm_le {f : α → G} {g : α → ℝ} (hg : Integrable g μ) (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ g x) :
    ‖∫ x, f x ∂μ‖ ≤ ∫ x, g x ∂μ :=
  calc
    ‖∫ x, f x ∂μ‖ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm f
    _ ≤ ∫ x, g x ∂μ := integral_mono_of_nonneg (Eventually.of_forall fun _ => norm_nonneg _) hg h

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