integrable_piLp_iff — Mathlib

English

For a PiLp-valued function f, integrability is equivalent to integrability of all coordinates.

Русский

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

LaTeX

$$$$\\text{Integrable}(f,\\mu) \\iff \\forall i, \\text{Integrable}(f\\cdot i,\\mu).$$$$

Lean4

theorem integrable_piLp_iff : Integrable f μ ↔ ∀ i, Integrable (f · i) μ := by
  simp_rw [← memLp_one_iff_integrable, memLp_piLp_iff]

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