# ℒp spaces and products #

source
theorem MeasureTheory.MemLp.comp_fst {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure α} {p : ENNReal} {f : α → ε} (hf : MemLp f p μ) (ν : Measure β) [IsFiniteMeasure ν] :
MemLp (fun (x : α × β) => f x.1) p (μ.prod ν)
source
theorem MeasureTheory.MemLp.comp_snd {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [TopologicalSpace ε] [ContinuousENorm ε] {ν : Measure β} {p : ENNReal} {f : β → ε} (hf : MemLp f p ν) (μ : Measure α) [IsFiniteMeasure μ] [SFinite ν] :
MemLp (fun (x : α × β) => f x.2) p (μ.prod ν)