integrable_iff — Mathlib

English

For simple functions, integrability is equivalent to the finite preimage measures of nonzero values.

Русский

Для простой функции интегрируемость эквивалентна конечной мере прообразов не нулевых значений.

LaTeX

$$$\\mathrm{Integrable}(f,\\mu) \\iff \\forall y\\,(y\\neq 0\\Rightarrow \\mu(f^{-1}(\\{y\\}))<\\infty)$$$

Lean4

theorem integrable_iff {f : α →ₛ E} : Integrable f μ ↔ ∀ y, y ≠ 0 → μ (f ⁻¹' { y }) < ∞ :=
  memLp_one_iff_integrable.symm.trans <| memLp_iff one_ne_zero ENNReal.coe_ne_top

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