memLp_prodLp_iff — Mathlib

English

Let f: X → WithLp q (Prod E F). Then f ∈ L^p iff both coordinates lie in L^p.

Русский

Пусть f: X → WithLp q (Prod E F). Тогда f ∈ L^p тогда и только тогда, когда обе координаты принадлежат L^p.

LaTeX

$$$$\\text{MemLp}(f,p,\\mu) \\iff \\text{MemLp}(\\lambda x. (f x).fst, p, \\mu) \\land \\text{MemLp}(\\lambda x. (f x).snd, p, \\mu).$$$$

Lean4

theorem memLp_prodLp_iff : MemLp f p μ ↔ MemLp (fun x ↦ (f x).fst) p μ ∧ MemLp (fun x ↦ (f x).snd) p μ :=
  by
  simp_rw [← memLp_prod_iff]
  exact
    (WithLp.prod_lipschitzWith_ofLp q E F).memLp_comp_iff_of_antilipschitz (WithLp.prod_antilipschitzWith_ofLp q E F)
        (by simp) |>.symm

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