Norm comparisons at a fixed time

The supremum-norm L² norms of the gradient and Hessian tensors are bounded by the square roots of the corresponding integrated sums of squares, and the Hessian energy equals the Laplacian energy at every time slice on which the second derivatives form a Sobolev family (lem:lps-H1-estimate).

theorem ESS.lps_h1_tensor_norm_sq_le (v : Fin 3 → CKN.Foundation.Parabolic.Vec3) : ‖v‖ ^ 2 ≤ ∑ i : Fin 3, ∑ j : Fin 3, v i j ^ 2

The supremum norm of a 3 × 3 tensor is bounded by the Frobenius norm.

theorem ESS.lps_h1_tensor3_norm_sq_le (w : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) : ‖w‖ ^ 2 ≤ ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, w i j k ^ 2

The supremum norm of a 3 × 3 × 3 tensor is bounded by the Frobenius norm.

theorem ESS.lps_h1_gradient_norm_le {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm Du 2 MeasureTheory.volume).toReal ≤ √(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du x i j ^ 2)

The L² norm of a tensor field of the first-derivative type is bounded by the square root of the integrated sum of squares of its entries.

theorem ESS.lps_h1_gradient_norm_sq_integral_le {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ‖Du x‖ ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du x i j ^ 2

The integrated squared supremum norm of a gradient tensor is bounded by the integrated sum of squares of its entries.

theorem ESS.lps_h1_hessian_norm_le {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm D2u 2 MeasureTheory.volume).toReal ≤ √(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2u x i j k ^ 2)

The L² norm of a second-derivative tensor field is bounded by the square root of the integrated sum of squares of its entries.

theorem ESS.lps_h1_slice_hessian_energy_eq {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} (hfam : ∀ (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) => LPS.lpsH1SpatialFamily u Du D2u i α (x, t)) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2u (x, t) i j k ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D2u (x, t) i j j) ^ 2

At a time slice where the second derivatives form a Sobolev family, the Hessian energy equals the Laplacian energy (lem:lps-H1-estimate).