Extension by zero between restricted Lᵖ spaces

An Lᵖ function on a measurable set s extends by zero to any larger set t ⊇ s, and the extension has the same Lᵖ norm, because the added region contributes nothing. This file bundles that extension as a linear isometry

TauCeti.extendByZeroLpₗᵢ 𝕜 μ hs hst : Lp F p (μ.restrict s) →ₗᵢ[𝕜] Lp F p (μ.restrict t),

together with the almost-everywhere description of its values, TauCeti.coeFn_extendByZeroLpₗᵢ.

The one point that needs care is that Lᵖ elements are equivalence classes: s.indicator ⇑f depends on the chosen representative ⇑f, which is only pinned down μ.restrict s-almost everywhere, whereas the answer must be pinned down μ.restrict t-almost everywhere. Mathlib's MeasureTheory.ae_eq_restrict_iff_indicator_ae_eq reconciles the two: an identity holding μ.restrict s-almost everywhere survives multiplication by the indicator of s as an identity against μ, hence against every restriction of μ.

Main declarations

• TauCeti.extendByZeroLpₗᵢ: extension by zero as a linear isometry.
• TauCeti.coeFn_extendByZeroLpₗᵢ and TauCeti.coeFn_extendByZeroLpₗᵢ_restrict: the values of the extension, on t and back on s.
• TauCeti.extendByZeroLpₗᵢ_self and TauCeti.extendByZeroLpₗᵢ_extendByZeroLpₗᵢ: extending along s ⊆ s is the identity, and extending twice is extending once.
• TauCeti.extendByZeroLpₗᵢ_eq_of_ae_eq and TauCeti.coeFn_extendByZeroLpₗᵢ_comp: the two ways an extension is recognised in practice — from a representative that already vanishes off s, and through pointwise postcomposition by a map fixing 0.

noncomputable def TauCeti.extendByZeroLpₗᵢ {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} (μ : MeasureTheory.Measure α) {s t : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (hst : s ⊆ t) : ↥(MeasureTheory.Lp F p (μ.restrict s)) →ₗᵢ[𝕜] ↥(MeasureTheory.Lp F p (μ.restrict t))

Extension by zero as a linear isometry Lᵖ(s) → Lᵖ(t) for a measurable s ⊆ t: a function on s is regarded as a function on the larger set t by declaring it zero on t \ s.

It is an isometry, not merely a bounded map, because the enlarged region contributes nothing to the Lᵖ norm; in particular the extension is injective, so Lᵖ(s) really does sit inside Lᵖ(t).

Equations

• TauCeti.extendByZeroLpₗᵢ 𝕜 μ hs hst = { toLinearMap := TauCeti.extendByZeroLpₗ✝ 𝕜 μ hs hst, norm_map' := ⋯ }

theorem TauCeti.coeFn_extendByZeroLpₗᵢ {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure α} {s t : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (hst : s ⊆ t) (f : ↥(MeasureTheory.Lp F p (μ.restrict s))) : ↑↑((extendByZeroLpₗᵢ 𝕜 μ hs hst) f) =ᵐ[μ.restrict t] s.indicator ↑↑f

The extension by zero is the indicator of the original representative.

theorem TauCeti.coeFn_extendByZeroLpₗᵢ_restrict {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure α} {s t : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (hst : s ⊆ t) (f : ↥(MeasureTheory.Lp F p (μ.restrict s))) : ↑↑((extendByZeroLpₗᵢ 𝕜 μ hs hst) f) =ᵐ[μ.restrict s] ↑↑f

The extension by zero restricts back to the original function.

@[simp]

theorem TauCeti.extendByZeroLpₗᵢ_self {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure α} {s : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (f : ↥(MeasureTheory.Lp F p (μ.restrict s))) : (extendByZeroLpₗᵢ 𝕜 μ hs ⋯) f = f

Extending by zero along s ⊆ s does nothing.

@[simp]

theorem TauCeti.extendByZeroLpₗᵢ_extendByZeroLpₗᵢ {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure α} {s t : Set α} [Fact (1 ≤ p)] {u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : s ⊆ t) (htu : t ⊆ u) (f : ↥(MeasureTheory.Lp F p (μ.restrict s))) : (extendByZeroLpₗᵢ 𝕜 μ ht htu) ((extendByZeroLpₗᵢ 𝕜 μ hs hst) f) = (extendByZeroLpₗᵢ 𝕜 μ hs ⋯) f

Extending by zero twice is extending by zero once. Zero-extending from s to t and then from t to u is the zero-extension from s to u.

theorem TauCeti.extendByZeroLpₗᵢ_eq_of_ae_eq {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure α} {s t : Set α} [Fact (1 ≤ p)] (hs : MeasurableSet s) (hst : s ⊆ t) {h : α → F} (hsupp : Function.support h ⊆ s) {f : ↥(MeasureTheory.Lp F p (μ.restrict s))} {g : ↥(MeasureTheory.Lp F p (μ.restrict t))} (hf : ∀ᵐ (x : α) ∂μ.restrict s, ↑↑f x = h x) (hg : ∀ᵐ (x : α) ∂μ.restrict t, ↑↑g x = h x) : (extendByZeroLpₗᵢ 𝕜 μ hs hst) f = g

Recognising an extension by zero from a common representative. A function h supported in s that represents f on s and g on t exhibits g as the zero-extension of f; this is how a function already known to vanish off s is transported from Lᵖ(s) to Lᵖ(t).

theorem TauCeti.coeFn_extendByZeroLpₗᵢ_comp {α : Type u_1} [MeasurableSpace α] {F : Type u_2} [NormedAddCommGroup F] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure α} {s t : Set α} {G : Type u_4} [NormedAddCommGroup G] [Module 𝕜 G] [IsBoundedSMul 𝕜 G] [Fact (1 ≤ p)] (hs : MeasurableSet s) (hst : s ⊆ t) (L : F → G) (hL : L 0 = 0) {f : ↥(MeasureTheory.Lp F p (μ.restrict s))} {g' : ↥(MeasureTheory.Lp G p (μ.restrict s))} (hg' : ∀ᵐ (x : α) ∂μ.restrict s, ↑↑g' x = L (↑↑f x)) : ↑↑((extendByZeroLpₗᵢ 𝕜 μ hs hst) g') =ᵐ[μ.restrict t] fun (x : α) => L (↑↑((extendByZeroLpₗᵢ 𝕜 μ hs hst) f) x)

Extension by zero commutes with pointwise postcomposition by a map fixing 0. If g' is the pointwise image of f under L, then the extension of g' is the pointwise image under L of the extension of f: off s both sides are L 0 = 0.