RellichKondrachov.MeasureTheory.Function.LpSpace.ExtendByZeroRangeEquiv #
Transport Lp extend-by-zero ranges across comparable measures on a measurable set.
For a measurable set s, the extend-by-zero map
Lp E p (μ.restrict s) →ₗᵢ[ℝ] Lp E p μ is a linear isometry. Hence its range is canonically
isomorphic to Lp E p (μ.restrict s). If two measures μ, ν are mutually comparable on s,
Lp.changeMeasureEquiv provides an equivalence between the restricted Lp spaces, and therefore
an equivalence between the corresponding extend-by-zero ranges.
This is used in the manifold Rellich glue to transport compactness on volume to chart measures on
fixed compact supports.
noncomputable def
MeasureTheory.Lp.extendByZeroRangeEquivOfRestrictChangeMeasureEquiv
{α : Type u_1}
[MeasurableSpace α]
{μ ν : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{p : ENNReal}
[Fact (1 ≤ p)]
{s : Set α}
(hs : MeasurableSet s)
{c₁ c₂ : ENNReal}
(hc₁ : c₁ ≠ ⊤)
(hc₂ : c₂ ≠ ⊤)
(hν : ν.restrict s ≤ c₁ • μ.restrict s)
(hμ : μ.restrict s ≤ c₂ • ν.restrict s)
(hp : p ≠ ⊤)
:
If μ.restrict s and ν.restrict s are mutually comparable (with finite constants), then the
extend-by-zero ranges in Lp are continuously linearly equivalent.
Equations
- One or more equations did not get rendered due to their size.