lintegral_edist_triangle — Mathlib

English

A function has finite integral if and only if the lintegral of its ENorm is finite: HasFiniteIntegral f μ ↔ ∫⁻ ‖f‖ dμ < ∞.

Русский

Функция имеет конечный интеграл тогда и только тогда, когда линтеграл ENorm от неё конечен.

LaTeX

$$$ \\text{HasFiniteIntegral} f \\mu \\iff \\int^- a \\, \\|f(a)\\|_{\\varepsilon} \\, d\\mu(a) < \\infty $$$

Lean4

theorem lintegral_edist_triangle {f g h : α → β} (hf : AEStronglyMeasurable f μ) (hh : AEStronglyMeasurable h μ) :
    (∫⁻ a, edist (f a) (g a) ∂μ) ≤ (∫⁻ a, edist (f a) (h a) ∂μ) + ∫⁻ a, edist (g a) (h a) ∂μ :=
  by
  rw [← lintegral_add_left' (hf.edist hh)]
  refine lintegral_mono fun a => ?_
  apply edist_triangle_right

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