Restriction of first-order Sobolev functions #
A weakly differentiable function on an open set remains weakly differentiable on every smaller
open set. This file packages that operation as the contractive continuous linear map
TauCeti.W1p.restrictL. Its value and weak gradient are represented by the same functions on
the smaller domain, and restriction is functorial.
Restriction is the basic localization operation for Sobolev spaces. In particular, it lets
interior regularity arguments pass from a weak solution on Ω to smaller open sets.
Main declarations #
TauCeti.W1p.restrictL: the contractive restriction map fromW^{1,p}(Ω)toW^{1,p}(U)forU ⊆ Ω.TauCeti.W1p.value_restrictLandTauCeti.W1p.gradient_restrictL: restriction commutes with the value and weak-gradient projections; their_aevariants identify representatives.TauCeti.W1p.restrictL_selfandTauCeti.W1p.restrictL_restrictL: restriction is functorial.TauCeti.W1p.continuous_setAverage_value: the mean of the value component over a fixed finite-measure subset depends continuously on the Sobolev function.
References #
L. C. Evans, Partial Differential Equations, Chapter 5, §5.2.
Restriction of ambient jets #
Restriction of an Lᵖ value-gradient jet to a smaller open set.
Equations
Instances For
Restricting an ambient jet keeps the same representative on the smaller open set.
Restriction of ambient jets does not increase the Lᵖ norm.
The value component of a restricted ambient jet is the restriction of its value component.
The gradient component of a restricted ambient jet is the restriction of its gradient component.
Restriction of Sobolev functions #
Restriction of first-order Sobolev functions. If U ⊆ Ω, this is the continuous
linear map W^{1,p}(Ω) → W^{1,p}(U) obtained by restricting both the value and weak gradient.
It has operator norm at most one.
Equations
- TauCeti.W1p.restrictL hU = (TauCeti.Sobolev1JetLp.restrictL hU ∘SL (↑(TauCeti.w1pSubmodule mu Omega p)).subtypeL).codRestrict ↑(TauCeti.w1pSubmodule mu U p) ⋯
Instances For
The ambient jet of a restricted Sobolev function is the restriction of its ambient jet.
The value component of a restricted Sobolev function is the restriction of its value component.
The gradient component of a restricted Sobolev function is the restriction of its gradient component.
Restriction keeps the same value representative on the smaller open set.
Restriction keeps the same weak-gradient representative on the smaller open set.
Restriction does not increase the Sobolev norm.
The restriction operator has norm at most one.
Restricting a Sobolev function to its original domain does nothing.
Restriction is functorial: restricting from Ω to U and then to V agrees with direct
restriction from Ω to V.
Subset averages #
The mean of the value of a first-order Sobolev function over a fixed subset of finite measure depends continuously on the function.