Precomposition by a map with dominated pushforward

Let f : α → β be almost everywhere measurable for μ. If μ.map f ≤ C • ν, then eLpNorm (g ∘ f) p μ ≤ C ^ (1/p) * eLpNorm g p ν for every p (MeasureTheory.eLpNorm_comp_le_of_map_le_smul). The codomain only needs a continuous extended norm. For a normed vector space codomain, C < ⊤, and 1 ≤ p, this estimate gives boundedness of precomposition from Lᵖ(ν) to Lᵖ(μ), with norm at most C ^ (1/p).

For a measure-preserving measurable embedding the bound is an equality, also after restricting to the preimage of an arbitrary set (MeasureTheory.MeasurePreserving.eLpNorm_comp_restrict_preimage).

For p = ∞ no bound on the pushforward is needed: precomposition with a quasi-measure-preserving map, such as the projection Prod.fst from a product of σ-finite measures, preserves L^∞ (MeasureTheory.MemLp.comp_quasiMeasurePreserving_top).

Main declarations

• MeasureTheory.eLpNorm_comp_le_of_map_le_smul: the eLpNorm bound for precomposition.
• MeasureTheory.MeasurePreserving.eLpNorm_comp_restrict_preimage, MeasureTheory.MeasurePreserving.memLp_comp_restrict_preimage_iff: a measure-preserving measurable embedding f identifies the Lᵖ seminorm of g ∘ f on f ⁻¹' s with that of g on s.
• MeasureTheory.MemLp.comp_quasiMeasurePreserving_top: precomposition with a quasi-measure-preserving map preserves L^∞.
• MeasureTheory.eLpNorm_clm_comp_le: postcomposition with a continuous linear map scales eLpNorm by at most its operator norm, with no measurability assumption.
• Homeomorph.memLp_comp_restrict_of_forall_isCompact: precomposition with a measure-preserving homeomorphism preserves Lᵖ integrability on compact subsets.

theorem MeasureTheory.eLpNorm_comp_le_of_map_le_smul {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure α} {ν : Measure β} {f : α → β} {g : β → ε} {C : ENNReal} (hf : AEMeasurable f μ) (hmap : Measure.map f μ ≤ C • ν) (p : ENNReal) : eLpNorm (g ∘ f) p μ ≤ C ^ (1 / p).toReal * eLpNorm g p ν

eLpNorm bound for precomposition. If f pushes μ forward to at most C • ν, then eLpNorm (g ∘ f) p μ ≤ C ^ (1/p) * eLpNorm g p ν. No measurability assumption on g is needed: its eLpNorm is infinite when it is not almost everywhere strongly measurable.

theorem MeasureTheory.MeasurePreserving.eLpNorm_comp_restrict_preimage {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure α} {ν : Measure β} {f : α → β} (hf : MeasurePreserving f μ ν) (he : MeasurableEmbedding f) (g : β → ε) (p : ENNReal) (s : Set β) : eLpNorm (g ∘ f) p (μ.restrict (f ⁻¹' s)) = eLpNorm g p (ν.restrict s)

Measure-preserving change of variables on a preimage. If f is a measurable embedding carrying μ to ν, then the Lᵖ seminorm of g ∘ f on f ⁻¹' s is that of g on s. Neither g nor s needs to be measurable.

theorem MeasureTheory.MeasurePreserving.memLp_comp_restrict_preimage_iff {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure α} {ν : Measure β} {f : α → β} (hf : MeasurePreserving f μ ν) (he : MeasurableEmbedding f) {g : β → ε} {p : ENNReal} {s : Set β} : MemLp (g ∘ f) p (μ.restrict (f ⁻¹' s)) ↔ MemLp g p (ν.restrict s)

Measure-preserving change of variables in Lᵖ on a preimage. If f is a measurable embedding carrying μ to ν, then g ∘ f is Lᵖ on f ⁻¹' s exactly when g is Lᵖ on s.

theorem MeasureTheory.MemLp.comp_quasiMeasurePreserving_top {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure α} {ν : Measure β} {f : α → β} {g : β → ε} (hg : MemLp g ⊤ ν) (hf : QuasiMeasurePreserving f μ ν) : MemLp (g ∘ f) ⊤ μ

Precomposition preserves L^∞. If g ∈ L^∞(ν) and f is quasi-measure-preserving from μ to ν, then g ∘ f ∈ L^∞(μ).

theorem MeasureTheory.eLpNorm_clm_comp_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {u : α → F} {p : ENNReal} (A : F →L[ℝ] G) : eLpNorm (fun (x : α) => A (u x)) p μ ≤ ‖A‖ₑ * eLpNorm u p μ

eLpNorm bound for postcomposition. A continuous linear map of the codomain scales eLpNorm by at most its operator norm. No measurability assumption is needed: a function that is not almost everywhere strongly measurable has infinite eLpNorm.

theorem Homeomorph.memLp_comp_restrict_of_forall_isCompact {α : Type u_1} {β : Type u_2} {ε : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [TopologicalSpace ε] [ContinuousENorm ε] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ₜ β) (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) {U : Set β} {g : β → ε} {p : ENNReal} (hg : ∀ (K : Set β), IsCompact K → K ⊆ U → MeasureTheory.MemLp g p (ν.restrict K)) {K : Set α} (hK : IsCompact K) (hKU : K ⊆ ⇑e ⁻¹' U) : MeasureTheory.MemLp (g ∘ ⇑e) p (μ.restrict K)

Local Lᵖ integrability under a measure-preserving homeomorphism. If g lies in Lᵖ(ν) on every compact subset of U and the homeomorphism e carries μ to ν, then g ∘ e lies in Lᵖ(μ) on every compact subset of e⁻¹(U).