ℒp spaces and products #
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 ν]
:
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 ν]
: