English
Let f: X → Π i, E_i be a measurable map into a finite product of normed spaces. Then f ∈ L^p(μ) if and only if each coordinate function f_i ∈ L^p(μ).
Русский
Пусть f: X → Π_i E_i — измеримая карта в конечном произведении нормированных пространств. Тогда 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_pi_iff : MemLp f p μ ↔ ∀ i, MemLp (f · i) p μ
where
mp hf i := (LipschitzWith.eval (α := E) i).comp_memLp rfl hf
mpr
hf := by
classical
have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
rw [this]
refine memLp_finset_sum' _ fun i _ ↦ ?_
exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)
