memLp_piLp_iff — Mathlib

English

Let f: X → PiLp q E be a map into a PiLp space; then f ∈ L^p iff each coordinate f·i ∈ L^p.

Русский

Пусть f: X → PiLp q E — отображение в пространство PiLp; тогда f ∈ L^p тогда и только тогда, когда каждая координата f_i ∈ L^p.

LaTeX

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

Lean4

theorem memLp_piLp_iff : MemLp f p μ ↔ ∀ i, MemLp (f · i) p μ :=
  by
  simp_rw [← PiLp.ofLp_apply, ← memLp_pi_iff, ← Function.comp_apply (f := WithLp.ofLp)]
  exact
    (PiLp.lipschitzWith_ofLp q E).memLp_comp_iff_of_antilipschitz (PiLp.antilipschitzWith_ofLp q E) (by simp) |>.symm

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