Iterated Lᵖ seminorms on a product measure

For a function f on α × β and an exponent p : ℝ≥0∞, taking the Lᵖ(ν) seminorm of each section y ↦ f (x, y) gives a function of x. This file shows that this function is almost-everywhere strongly measurable as soon as f is, and that its Lᵖ(μ) seminorm is the Lᵖ(μ ⊗ ν) seminorm of f. For 0 < p < ∞ this is Tonelli's theorem applied to ‖f‖ₑ ^ p; at p = ∞ it says that the essential supremum over the product is the iterated essential supremum. Only the second measure needs to be s-finite.

Main statements

• Measurable.eLpNorm_prod_right and MeasureTheory.AEStronglyMeasurable.eLpNorm_prod_right — the section seminorms x ↦ ‖f (x, ·)‖_{Lᵖ(ν)} form a measurable, respectively almost-everywhere strongly measurable, function;
• TauCeti.eLpNorm_prod_eq_eLpNorm_eLpNorm — the Lᵖ(μ ⊗ ν) seminorm of f is the Lᵖ(μ) seminorm of its section seminorms.
• TauCeti.eLpNorm_prod_smul — the Lᵖ(μ ⊗ ν) seminorm of (x, y) ↦ f x • g y is the product of the Lᵖ(μ) seminorm of f and the Lᵖ(ν) seminorm of g.
• MeasureTheory.MemLp.ae_memLp_prod_right — for f ∈ Lᵖ(μ ⊗ ν), almost every section is in Lᵖ(ν).

@[simp]

theorem TauCeti.eLpNorm_exponent_top_toFinite {β : Type u_2} {ε : Type u_3} [MeasurableSpace β] [TopologicalSpace ε] {ν : MeasureTheory.Measure β} [ENorm ε] [MeasureTheory.SFinite ν] (g : β → ε) : MeasureTheory.eLpNorm g ⊤ ν.toFinite = MeasureTheory.eLpNorm g ⊤ ν

The L^∞ seminorm only sees the null sets of the measure, so it does not change when an s-finite measure is replaced by the equivalent finite measure Measure.toFinite.

theorem Measurable.eLpNorm_prod_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {p : ENNReal} [MeasureTheory.SFinite ν] {g : α × β → ENNReal} (hg : Measurable g) : Measurable fun (x : α) => MeasureTheory.eLpNorm (fun (y : β) => g (x, y)) p ν

For a measurable g : α × β → ℝ≥0∞ and an s-finite ν, the section seminorms x ↦ ‖g (x, ·)‖_{Lᵖ(ν)} form a measurable function, for every exponent including p = ∞.

theorem MeasureTheory.AEStronglyMeasurable.eLpNorm_prod_right {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] {μ : Measure α} {ν : Measure β} {p : ENNReal} [ContinuousENorm ε] [SFinite ν] {f : α × β → ε} (hf : AEStronglyMeasurable f (μ.prod ν)) : AEStronglyMeasurable (fun (x : α) => eLpNorm (fun (y : β) => f (x, y)) p ν) μ

For an almost-everywhere strongly measurable f on μ ⊗ ν, the section seminorms x ↦ ‖f (x, ·)‖_{Lᵖ(ν)} form an almost-everywhere strongly measurable function, for every exponent including p = ∞.

theorem TauCeti.eLpNorm_prod_eq_eLpNorm_eLpNorm {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {p : ENNReal} [ContinuousENorm ε] [MeasureTheory.SFinite ν] {f : α × β → ε} (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) : MeasureTheory.eLpNorm f p (μ.prod ν) = MeasureTheory.eLpNorm (fun (x : α) => MeasureTheory.eLpNorm (fun (y : β) => f (x, y)) p ν) p μ

Iterated Lᵖ seminorms. The Lᵖ(μ ⊗ ν) seminorm of an almost-everywhere strongly measurable function is the Lᵖ(μ) seminorm of its section seminorms x ↦ ‖f (x, ·)‖_{Lᵖ(ν)}. This holds for every exponent, including p = ∞, where it identifies the essential supremum over the product with the iterated essential supremum.

theorem TauCeti.eLpNorm_prod_smul {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {p : ENNReal} [ContinuousENorm ε] [MeasureTheory.SFinite ν] {𝕜 : Type u_4} [TopologicalSpace 𝕜] [ContinuousENorm 𝕜] [SMul 𝕜 ε] [ContinuousSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] {f : α → 𝕜} {g : β → ε} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g ν) : MeasureTheory.eLpNorm (fun (z : α × β) => f z.1 • g z.2) p (μ.prod ν) = MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g p ν

The Lᵖ seminorm of a tensor product. The Lᵖ(μ ⊗ ν) seminorm of (x, y) ↦ f x • g y is the product of the Lᵖ(μ) seminorm of f and the Lᵖ(ν) seminorm of g, for every exponent, including p = ∞. The scalar action need only be continuous and satisfy ‖c • v‖ₑ = ‖c‖ₑ * ‖v‖ₑ.

theorem MeasureTheory.MemLp.ae_memLp_prod_right {α : Type u_1} {β : Type u_2} {ε : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace ε] {μ : Measure α} {ν : Measure β} {p : ENNReal} [ContinuousENorm ε] [SFinite ν] {f : α × β → ε} (hf : MemLp f p (μ.prod ν)) : ∀ᵐ (x : α) ∂μ, MemLp (fun (y : β) => f (x, y)) p ν

If f ∈ Lᵖ(μ ⊗ ν) then almost every section y ↦ f (x, y) is in Lᵖ(ν).