The nonlinear pairing in the strong H¹ estimate

The finite-Serrin spatial interpolation controls the convection term paired with a square-integrable Laplacian (lem:lps-H1-estimate).

theorem ESS.LPS.lps_h1_laplacian_memLp_two {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {lap : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hD2u : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hlap : ∀ (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3), lap x i = ∑ j : Fin 3, D2u x i j j) : MeasureTheory.MemLp lap 2 MeasureTheory.volume

The componentwise trace of a square-integrable Hessian is a square-integrable vector field (lem:lps-H1-estimate).

theorem ESS.LPS.lps_h1_smooth_hessian_eq_laplacian {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hu : ContDiff ℝ (↑⊤) u) (huc : HasCompactSupport u) : ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.mixedSecond (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j k x ^ 2 = ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x ^ 2

For a smooth compactly supported vector field, the summed squared Hessian norm equals the squared vector-Laplacian norm componentwise. This is the dense smooth case of the whole-space H² bridge in lem:lps-H1-estimate.

theorem ESS.LPS.lps_h1_finite_nonlinear_pairing_bound {s : ℝ} (hs : 3 < s) {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {lap : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (huMeas : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (huS : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) (ENNReal.ofReal s) MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) (k : Fin 3) => D2u x i j k) (hlap : ∀ (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3), lap x i = ∑ j : Fin 3, D2u x i j j) : |∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, u x j * Du x i j) * lap x i| ≤ 243 * CKN.gagliardoNirenbergSobolevConstant.toReal ^ (3 / s) * 2 ^ (3 / s) * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) (ENNReal.ofReal s) MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm Du 2 MeasureTheory.volume).toReal ^ ((s - 3) / s) * (MeasureTheory.eLpNorm D2u 2 MeasureTheory.volume).toReal ^ (1 + 3 / s)

At almost every strong H² slice, the finite Serrin interpolation bounds the convection term paired with the Laplacian. This is the spatial estimate used before Young absorption in lem:lps-H1-estimate.

theorem ESS.LPS.lps_h1_infinite_nonlinear_pairing_bound {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {lap : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (huMeas : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (huInf : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) ⊤ MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hlap2 : MeasureTheory.MemLp lap 2 MeasureTheory.volume) : |∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, u x j * Du x i j) * lap x i| ≤ 9 * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) ⊤ MeasureTheory.volume).toReal * √(∫ (x : CKN.Foundation.Parabolic.Vec3), ‖Du x‖ ^ 2) * √(∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (lap x) ^ 2)

The endpoint (s = ∞) convection term paired with the vector Laplacian is controlled by the spatial essential supremum and the two L² factors. This is the spatial estimate used before endpoint Young absorption in lem:lps-H1-estimate.