Fixed-time endpoint convection estimates

The endpoint slice estimate bounds the relative convection by the gradient energy and the squared spatial L∞ coefficient. The trilinear companion gives the majorant used in the endpoint density passage (lem:lps-comparison).

theorem ESS.lps_endpoint_relative_convection_slice {u w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → 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) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hDw2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) : |∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * ∑ j : Fin 3, w x j * Dw x i j| ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Dw x i j ^ 2) + 81 / 2 * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) ⊤ MeasureTheory.volume).toReal ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, w x i ^ 2 ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (w x) * √(∑ i : Fin 3, ∑ j : Fin 3, Dw x i j ^ 2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (u x) ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), √(∑ i : Fin 3, ∑ j : Fin 3, Dw x i j ^ 2) ^ 2) + (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (w x) ^ 2) * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) ⊤ MeasureTheory.volume).toReal ^ 2

The fixed-time endpoint estimates for a convection difference.