Extension by zero as an Lp isometry

For a measurable set s, extension by zero identifies Lᵖ on the restricted measure μ.restrict s with the subspace of Lᵖ μ of functions supported in s. The map f ↦ s.indicator f preserves the Lᵖ norm, because the seminorm on μ.restrict s equals the seminorm of the indicator on μ. We package it as a linear isometry MeasureTheory.lpExtendByZero.

This is the bridge that lets a compact-embedding argument on a bounded domain Ω be run in the ambient space Lᵖ(ℝⁿ): a class on L²(Ω) = Lp ℝ 2 (volume.restrict Ω) is sent to its extension by zero in L²(ℝⁿ) = Lp ℝ 2 volume, where the Fréchet-Kolmogorov criterion applies.

Main definitions

• MeasureTheory.lpExtendByZero: extension by zero Lp ℝ p (μ.restrict s) →ₗᵢ[ℝ] Lp ℝ p μ.

theorem MeasureTheory.memLp_indicator_extend {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {p : ENNReal} {s : Set α} (hs : MeasurableSet s) (f : ↥(Lp ℝ p (μ.restrict s))) : MemLp (s.indicator ↑↑f) p μ

The indicator of a class on the restricted measure is p-integrable for the full measure.

noncomputable def MeasureTheory.lpExtendByZero {α : Type u_1} [MeasurableSpace α] (μ : Measure α) (p : ENNReal) (s : Set α) [Fact (1 ≤ p)] (hs : MeasurableSet s) : ↥(Lp ℝ p (μ.restrict s)) →ₗᵢ[ℝ] ↥(Lp ℝ p μ)

Extension by zero as a linear isometry Lp ℝ p (μ.restrict s) →ₗᵢ[ℝ] Lp ℝ p μ. A class on the restricted measure is sent to the Lp class of its extension by zero, with the Lp norm preserved.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.coeFn_lpExtendByZero {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {p : ENNReal} {s : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (f : ↥(Lp ℝ p (μ.restrict s))) : ↑↑((lpExtendByZero μ p s hs) f) =ᵐ[μ] s.indicator ↑↑f

The extension by zero is represented almost everywhere by the indicator of s.

theorem MeasureTheory.lpExtendByZero_ae_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {p : ENNReal} {s : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (f : ↥(Lp ℝ p (μ.restrict s))) : ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑((lpExtendByZero μ p s hs) f) x = 0

The extension by zero is almost everywhere zero off s.