The relative convection bound at a fixed time

At a fixed time the relative convection form ∑ₖ uₖ ∑ⱼ wⱼ ∂ⱼ wₖ is bounded by half the dissipation of w plus a multiple of ‖u‖₅⁵ ‖w‖₂², by Hölder's inequality, the three-dimensional interpolation ‖w‖_{10/3} ≲ ‖w‖₂^{2/5} ‖∇w‖₂^{3/5} and Young's inequality with exponents 5/4 and 5. This is the Gronwall coefficient bound of lem:pv-serrin-uniqueness.

theorem ESS.serrin_slice_relative_bound : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {u w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}, MeasureTheory.MemLp u (ENNReal.ofReal 5) MeasureTheory.volume → MeasureTheory.MemLp w 2 MeasureTheory.volume → MeasureTheory.MemLp Dw 2 MeasureTheory.volume → (∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i) → |∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u x k * ∑ j : Fin 3, w x j * Dw x k j| ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, ∑ j : Fin 3, Dw x k j ^ 2) + K * (MeasureTheory.eLpNorm u (ENNReal.ofReal 5) MeasureTheory.volume).toReal ^ 5 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, w x k ^ 2

The Gronwall bound for the relative convection form at a fixed time.