hasFiniteIntegral_iff_edist — Mathlib

English

A function f has finite integral iff the lintegral of edist(f(a), 0) is finite.

Русский

Функция f имеет конечный интеграл тогда и только тогда, когда линтеграл edist(f(a), 0) конечен.

LaTeX

$$$ \\text{HasFiniteIntegral} f \\mu \\iff \\int^- a \\, \\mathrm{edist}(f(a), 0) \\, d\\mu(a) < \\infty $$$

Lean4

theorem hasFiniteIntegral_iff_edist (f : α → β) : HasFiniteIntegral f μ ↔ (∫⁻ a, edist (f a) 0 ∂μ) < ∞ := by
  simp only [hasFiniteIntegral_iff_norm, edist_dist, dist_zero_right]

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