theorem
MeasureTheory.eLpNormEssSup_map_measure'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
[MeasurableSpace E]
[OpensMeasurableSpace E]
(hg : AEMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_map_measure'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
[MeasurableSpace E]
[OpensMeasurableSpace E]
(hg : AEMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_comp_measurePreserving'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : Measure β}
[MeasurableSpace E]
[OpensMeasurableSpace E]
(hg : AEMeasurable g ν)
(hf : MeasurePreserving f μ ν)
: