RellichKondrachov.MeasureTheory.Function.LpSpace.Restrict #
L^p extension-by-zero maps for restricted measures.
Mathlib provides the equivalence
MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)
(MeasureTheory.memLp_indicator_iff_restrict). This file packages the corresponding map on Lp
spaces:
Lp E p (μ.restrict s) →ₗᵢ[ℝ] Lp E p μ,
given by extension-by-zero (via Set.indicator).
Main definitions #
noncomputable def
MeasureTheory.Lp.extendByZeroₗ
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{p : ENNReal}
{s : Set α}
(hs : MeasurableSet s)
:
Extension-by-zero as a linear map Lp E p (μ.restrict s) →ₗ[ℝ] Lp E p μ.
Equations
- MeasureTheory.Lp.extendByZeroₗ hs = { toFun := MeasureTheory.Lp.extendByZeroFun✝ hs, map_add' := ⋯, map_smul' := ⋯ }
Instances For
noncomputable def
MeasureTheory.Lp.extendByZeroₗᵢ
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{p : ENNReal}
[Fact (1 ≤ p)]
{s : Set α}
(hs : MeasurableSet s)
:
Extension-by-zero as a linear isometry.
Equations
- MeasureTheory.Lp.extendByZeroₗᵢ hs = { toLinearMap := MeasureTheory.Lp.extendByZeroₗ hs, norm_map' := ⋯ }
Instances For
theorem
MeasureTheory.Lp.extendByZeroₗᵢ_ae_eq
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{p : ENNReal}
[Fact (1 ≤ p)]
{s : Set α}
(hs : MeasurableSet s)
(f : ↥(Lp E p (μ.restrict s)))
:
↑↑((extendByZeroₗᵢ hs) f) =ᵐ[μ] s.indicator fun (x : α) => ↑↑f x
theorem
MeasureTheory.Lp.extendByZeroₗᵢ_congr
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{p : ENNReal}
[Fact (1 ≤ p)]
{s : Set α}
(hs₁ hs₂ : MeasurableSet s)
: