lintegral_nnnorm_le — Mathlib

English

For a bounded continuous f: X → E with normed target, the lintegral of the norm is bounded by the NNReal norm of f times the measure of the space.

Русский

Для ограниченной непрерывной f: X → E с нормой на целевой группе линегральный интеграл нормы ограничен нормой f в NNReal, умноженной на меру пространства.

LaTeX

$$$$\\int⁻ x, \\|f(x)\\|_+ ∂μ ≤ \\|f\\|_+ \\cdot (μ Set.univ).$$$$

Lean4

theorem lintegral_nnnorm_le (f : X →ᵇ E) : ∫⁻ x, ‖f x‖₊ ∂μ ≤ ‖f‖₊ * (μ Set.univ) := by
  calc
    ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ∫⁻ _, ‖f‖₊ ∂μ := by gcongr; apply nnnorm_coe_le_nnnorm
    _ = ‖f‖₊ * (μ Set.univ) := by rw [lintegral_const]

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