Relative convection on almost every slice

The finite Serrin assumption and the weak slice properties put the relative convection into the fixed-time Hölder, interpolation, and Young estimate.

theorem ESS.lps_finite_relative_convection_bound_ae {T s : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T a v Dv pv) (hs : 3 < s) (hmix : ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRelativeConvection u v Du Dv (x, t) ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRelativeGradientSq Du Dv (x, t)) + lpsPowerYoungCoefficient (3 / s) * (9 * (6 * CKN.gagliardoNirenbergSobolevConstant.toReal) ^ (3 / s)) ^ (2 * s / (s - 3)) * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal s) MeasureTheory.volume).toReal ^ (2 * s / (s - 3)) * lpsComparisonDistanceSq u v t

The finite Serrin branch supplies the fixed-time relative convection estimate on almost every slice, with a coefficient independent of time.