Trilinear identities at a fixed time

For slices u ∈ L² ∩ L⁵ and v ∈ L² ∩ L^{10/3} with square-integrable weak gradients of vanishing trace, the self-transport form of u vanishes, and the sum of the two convection pairings equals the relative convection form ∑ₖ uₖ ∑ⱼ (vⱼ - uⱼ)(∂ⱼ vₖ - ∂ⱼ uₖ). These reduce the cross-testing identity to the relative energy inequality of lem:pv-serrin-uniqueness.

theorem ESS.serrin_prod_memLp {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} {p q r : ℝ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (h : p⁻¹ + q⁻¹ = r⁻¹) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) (hg : MeasureTheory.MemLp g (ENNReal.ofReal q) MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) (ENNReal.ofReal r) MeasureTheory.volume

structure ESS.SerrinSlice (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) : Prop

The slice facts used in the trilinear identities.

• mem2 : MeasureTheory.MemLp w 2 MeasureTheory.volume
• grad2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume
• grad (i : Fin 3) : CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i
• trace : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Dw x j j = 0

theorem ESS.serrin_ofReal_two : 2 = ENNReal.ofReal 2

theorem ESS.serrin_slice_self_transport {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu : SerrinSlice u Du) (hu5 : MeasureTheory.MemLp u (ENNReal.ofReal 5) 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.

theorem ESS.serrin_slice_relative {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) (hu5 : MeasureTheory.MemLp u (ENNReal.ofReal 5) MeasureTheory.volume) (hv : SerrinSlice v Dv) (hv103 : MeasureTheory.MemLp v (ENNReal.ofReal (10 / 3)) 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 sum of the two convection pairings minus the relative convection form integrates to zero.