Endpoint Trilinear

The endpoint (s = ∞) spatial Hölder--Young estimate. The velocity field v is controlled in spatial L∞; the gradient term is the Frobenius norm of the explicit slice gradient Du (lem:lps-comparison).

theorem ESS.lps_slice_trilinear_bound_infinite {u v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hvMeas : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume) (hDuMeas : MeasureTheory.AEStronglyMeasurable Du MeasureTheory.volume) (hDuEntry2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Du x i j) 2 MeasureTheory.volume) (hvInf : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v x)) ⊤ MeasureTheory.volume < ⊤) : ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (u x) * √(∑ i : Fin 3, ∑ j : Fin 3, Du x i j ^ 2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v x) ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), √(∑ i : Fin 3, ∑ j : Fin 3, Du x i j ^ 2) ^ 2) + (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 2) * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v x)) ⊤ MeasureTheory.volume).toReal ^ 2

The endpoint (s = ∞) spatial Hölder--Young estimate. The velocity field v is controlled in spatial L∞; the gradient term is the Frobenius norm of the explicit slice gradient Du (lem:lps-comparison).