Sobolev families of the components of a strong solution #
prop:lps-smoothing: the weak first and second spatial derivatives of a strong solution
form an L²(I; H²) family for each velocity component.
def
ESS.lpsStrongFamily
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(i : Fin 3)
:
The ordered family of a velocity component through order two: the component itself, its
first derivatives Du z i j = ∂ⱼuᵢ and its second derivatives D2u z i j k = ∂ₖ∂ⱼuᵢ.
Equations
- ESS.lpsStrongFamily u Du D2u i [] = fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i
- ESS.lpsStrongFamily u Du D2u i [j] = fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z i j
- ESS.lpsStrongFamily u Du D2u i [j, k] = fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => D2u z i j k
- ESS.lpsStrongFamily u Du D2u i x✝ = fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0
Instances For
theorem
ESS.lps_strong_isL2SobolevFamily
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu)
(hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(i : Fin 3)
:
CKN.IsL2SobolevFamilyOn 2 Set.univ (Set.Ioo t₀ T) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i)
(lpsStrongFamily u Du D2u i)
The weak derivatives of a strong solution form an L²(I; H²) family for each velocity
component (prop:lps-smoothing).