Restriction of arbitrary-order Sobolev functions #

Restriction to an open subdomain is a contraction on W^{k,p} for every natural order k and every 1 ≤ p ≤ ∞. It commutes with the value, lower-order, and highest weak derivative projections. This supplies localization for smooth approximation and interior estimates without any boundary regularity assumption.

The construction uses W1p.restrictL at first order and restricts the successive weak derivative fields through Mathlib's Lp.LpToLpOfMeasureLeSMul.

References #

L. C. Evans, Partial Differential Equations, Chapter 5, §§5.2–5.3.

source

noncomputable def TauCeti.Wkp.restrictL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hU : U ≤ Omega) (k : ℕ) :

Wkp mu Omega p k →L[ℝ ] Wkp mu U p k

Restrict an arbitrary-order weak Sobolev function to an open subdomain. This continuous linear map has operator norm at most one.

Equations

TauCeti.Wkp.restrictL hU k = { toFun := TauCeti.Wkp.restrictAux✝ hU k, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

Instances For

source

@[simp]

theorem TauCeti.Wkp.value_restrictL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hU : U ≤ Omega) (k : ℕ) (u : Wkp mu Omega p k) :

value k ((restrictL hU k) u) = (MeasureTheory.Lp.LpToLpOfMeasureLeSMul value_restrictL._proof_1 ⋯) (value k u)

Restriction commutes with the Lᵖ value projection.

source

theorem TauCeti.Wkp.value_restrictL_ae {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hU : U ≤ Omega) (k : ℕ) (u : Wkp mu Omega p k) :

↑↑(value k ((restrictL hU k) u)) =ᵐ[mu.restrict ↑U] ↑↑(value k u)

Restriction keeps the same value representative on the smaller domain.

source

theorem TauCeti.Wkp.iteratedGradient_restrictL_ae {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hU : U ≤ Omega) (k : ℕ) (u : Wkp mu Omega p (k + 1)) :

↑↑(iteratedGradient k ((restrictL hU (k + 1)) u)) =ᵐ[mu.restrict ↑U] ↑↑(iteratedGradient k u)

Restriction keeps the same highest weak derivative on the smaller domain.

source

theorem TauCeti.Wkp.iteratedGradient_restrictL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hU : U ≤ Omega) (k : ℕ) (u : Wkp mu Omega p (k + 1)) :

iteratedGradient k ((restrictL hU (k + 1)) u) = (MeasureTheory.Lp.LpToLpOfMeasureLeSMul value_restrictL._proof_1 ⋯) (iteratedGradient k u)

Restriction commutes with the highest weak derivative projection. Use rw with this lemma: simp does not match its dependently indexed left-hand side.

source