Endpoint relative convection estimate

At the spatial endpoint, Hölder with exponents ∞, 2, 2 and Young's inequality give the fixed-time estimate needed in lem:lps-comparison.

theorem ESS.lps_slice_relative_bound_infty {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

Fixed-time relative convection estimate for the spatial endpoint. The coefficient is the square of the distinguished field's spatial L∞ norm, as in lem:lps-comparison.