Self-transport cancellation at the L⁴ exponent

The divergence-free transport pairing vanishes for an H¹ slice in L⁴.

theorem ESS.lps_slice_self_transport_four {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu : SerrinSlice u Du) (hu4 : MeasureTheory.MemLp u (ENNReal.ofReal 4) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u x k * ∑ j : Fin 3, u x j * Du x k j = 0

The self-transport form of an L⁴ slice vanishes.