English
Let f: X → WithLp q (E × F). Then f ∈ L^p if and only if its first and second components lie in L^p.
Русский
Пусть f: X → WithLp q (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_prod_iff : MemLp f p μ ↔ MemLp (fun x ↦ (f x).fst) p μ ∧ MemLp (fun x ↦ (f x).snd) p μ
where
mp h := ⟨LipschitzWith.prod_fst.comp_memLp (by simp) h, LipschitzWith.prod_snd.comp_memLp (by simp) h⟩
mpr
h :=
by
have : f = (AddMonoidHom.inl E F) ∘ (fun x ↦ (f x).fst) + (AddMonoidHom.inr E F) ∘ (fun x ↦ (f x).snd) := by ext;
all_goals simp
rw [this]
exact MemLp.add (Isometry.inl.lipschitz.comp_memLp (by simp) h.1) (Isometry.inr.lipschitz.comp_memLp (by simp) h.2)
