Uniqueness and restriction of Sobolev families #
prop:lps-smoothing: a Sobolev family through order M is a Sobolev family through every
smaller order, and two space-time Sobolev families of the same function, of possibly different
orders, agree almost everywhere on the slab through the smaller order.
theorem
CKN.IsSobolevFamilyOn.mono_order
{m M : ℕ}
{U : Set Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.Vec3 → ℝ}
{D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ}
(h : IsSobolevFamilyOn M U f D)
(hm : m ≤ M)
:
IsSobolevFamilyOn m U f D
A Sobolev family through order M is a Sobolev family through every smaller order
(prop:lps-smoothing).
theorem
ESS.lps_l2SobolevFamily_unique
{M M' : ℕ}
{I : Set ℝ}
(hI : IsOpen I)
{z : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{D D' : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(h : CKN.IsL2SobolevFamilyOn M Set.univ I z D)
(h' : CKN.IsL2SobolevFamilyOn M' Set.univ I z D')
(α : List (Fin 3))
:
Uniqueness of weak spatial derivatives on a slab: two space-time Sobolev families of the same
function, through orders M and M', agree almost everywhere on the slab through every order
at most M and M' (prop:lps-smoothing).