norm_integral_le_mul_norm — Mathlib

English

Under finite measure μ and normed target, the integral norm is bounded by the product of μ(univ) and the norm of f.

Русский

При конечной мере μ и нормированном целевом пространстве интегральная норма ограничена произведением μ(univ) на норму f.

LaTeX

$$$$\\|\\int x, f(x) ∂μ\\| ≤ (μ.univ) \\cdot \\|f\\|.$$$

Lean4

theorem norm_integral_le_mul_norm [IsFiniteMeasure μ] (f : X →ᵇ E) : ‖∫ x, f x ∂μ‖ ≤ μ.real Set.univ * ‖f‖ :=
  by
  calc
    ‖∫ x, f x ∂μ‖
    _ ≤ ∫ x, ‖f x‖ ∂μ := (norm_integral_le_integral_norm _)
    _ ≤ ∫ _, ‖f‖ ∂μ := ?_
    _ = μ.real Set.univ • ‖f‖ := by rw [integral_const]
  apply
    integral_mono _ (integrable_const ‖f‖)
      (fun x ↦ f.norm_coe_le_norm x) -- NOTE: `gcongr`?

  exact (integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ)

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