Relative Cancellation

The advective cross terms reduce to the relative convection form for a finite Serrin pair. The proof uses only the integrable products |u||v||Du|, |u|²|Du|, and |v||u||Du| (lem:lps-comparison).

theorem ESS.lps_slice_relative_cancellation {s : ℝ} (hs : 3 < s) {u v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu : SerrinSlice u Du) (huS : MeasureTheory.MemLp u (ENNReal.ofReal s) MeasureTheory.volume) (huQ : MeasureTheory.MemLp u (ENNReal.ofReal (2 * s / (s - 2))) MeasureTheory.volume) (hv : SerrinSlice v Dv) (hvQ : MeasureTheory.MemLp v (ENNReal.ofReal (2 * s / (s - 2))) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u x k * ∑ j : Fin 3, v x j * Dv x k j + ∑ k : Fin 3, v x k * ∑ j : Fin 3, u x j * Du x k j - ∑ k : Fin 3, u x k * ∑ j : Fin 3, (v x j - u x j) * (Dv x k j - Du x k j) = 0

The advective cross terms reduce to the relative convection form for a finite Serrin pair. The proof uses only the integrable products |u||v||Du|, |u|²|Du|, and |v||u||Du| (lem:lps-comparison).