memLp_iff — Mathlib

English

For 0<p<∞, MemLp f p μ iff the nonzero values y satisfy μ(f^{-1}({y}))<∞.

Русский

Для 0<p<∞ верно: MemLp f p μ эквивалентно тому, что для всех y≠0 выполняется μ(f^{-1}({y}))<∞.

LaTeX

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

Lean4

theorem memLp_iff {f : α →ₛ E} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) : MemLp f p μ ↔ ∀ y, y ≠ 0 → μ (f ⁻¹' { y }) < ∞ :=
  ⟨fun h => measure_preimage_lt_top_of_memLp hp_pos hp_ne_top f h, fun h => memLp_of_finite_measure_preimage p h⟩

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