The whole-space weak H² Hessian and Laplacian identity

Smooth compactly supported Sobolev approximations extend the Hessian/Laplacian identity to the whole-space order-two class used by lem:lps-H1-estimate.

def ESS.LPS.lpsH1SpatialFamily (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) : List (Fin 3) → CKN.Foundation.Parabolic.ParabolicPoint → ℝ

The order-zero, first and second spatial derivative fields of a component of a strong solution, indexed by derivative words.

Equations

• ESS.LPS.lpsH1SpatialFamily u Du D2u i [] = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z i
• ESS.LPS.lpsH1SpatialFamily u Du D2u i [j] = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Du z i j
• ESS.LPS.lpsH1SpatialFamily u Du D2u i [j, k] = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => D2u z i j k
• ESS.LPS.lpsH1SpatialFamily u Du D2u i x✝ = fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0

theorem ESS.LPS.lps_spatial_sobolev_slices_ae_of_weak_derivs {a b : ℝ} {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} (hDerivs : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo a b) u Du D2u Dtu) (hMemU : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hMemDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hMemD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i : Fin 3), CKN.IsSobolevFamilyOn 2 Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) fun (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3) => lpsH1SpatialFamily u Du D2u i α (x, t)

Space-time weak derivatives with square-integrable fields give spatial order-two Sobolev families on almost every time slice (lem:lps-H1-estimate).

theorem ESS.LPS.lps_strong_solution_h2_slices_ae {a b : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsLpsStrongSolution a b u Du p) : ∃ (D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo a b) u Du D2u Dtu ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i : Fin 3), CKN.IsSobolevFamilyOn 2 Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) fun (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3) => lpsH1SpatialFamily u Du D2u i α (x, t)

The space-time derivative witnesses in the strong class give spatial order-two Sobolev families on almost every time slice (lem:lps-H1-estimate).

theorem ESS.LPS.lps_h1_sobolev_hessian_eq_laplacian {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : CKN.IsSobolevFamilyOn 2 Set.univ f D) : ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), D [i, j] x ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ i : Fin 3, D [i, i] x) ^ 2

For a scalar whole-space order-two Sobolev family, the L² Hessian square equals the L² Laplacian square (lem:lps-H1-estimate).

theorem ESS.LPS.lps_h1_vector_sobolev_hessian_eq_laplacian {D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : ∀ (i : Fin 3), CKN.IsSobolevFamilyOn 2 Set.univ (D i []) (D i)) : ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), D i [j, k] x ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D i [j, j] x) ^ 2

The componentwise whole-space order-two Sobolev bridge identifies the integrated Hessian square with the vector Laplacian square (lem:lps-H1-estimate).