lintegral_edist_lt_top — Mathlib

English

If f and g are integrable, then the L^1-distance between f and g is finite.

Русский

Если f и g интегрируемы, то расстояние в L^1 между f и g конечна.

LaTeX

$$$\\int \\! edist(f, g) \\, dμ < ∞$ for integrable f, g.$$

Lean4

theorem lintegral_edist_lt_top {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
    (∫⁻ a, edist (f a) (g a) ∂μ) < ∞ :=
  lt_of_le_of_lt (lintegral_edist_triangle hf.aestronglyMeasurable aestronglyMeasurable_zero)
    (ENNReal.add_lt_top.2 <| by
      simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]
      exact ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩)

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