integrable — Mathlib

English

For a bounded continuous f: X → E, the norm of the integral is bounded by the measure times the norm of f, i.e., ∥∫ f∥ ≤ μ.univ · ∥f∥.

Русский

Для ограниченной непрерывной f: X → E выполнено неравенство ∥∫ f∥ ≤ μ(univ) · ∥f∥.

LaTeX

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

Lean4

theorem integrable [IsFiniteMeasure μ] (f : X →ᵇ E) : Integrable f μ :=
  by
  refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩
  calc
    ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ‖f‖₊ * (μ Set.univ) := (f.lintegral_nnnorm_le μ)
    _ < ∞ := ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top μ Set.univ)

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