Endpoint fixed-time relative convection bound #
At almost every time the relative convection is bounded by half the relative
gradient energy plus the squared L∞ norm of the distinguished velocity times
the relative slice energy (lem:lps-comparison, endpoint case).
theorem
ESS.lps_endpoint_relative_slice_bound
{T : ℝ}
{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)
(hEndpoint :
∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤)
:
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRelativeConvection u v Du Dv (x, τ) ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRelativeGradientSq Du Dv (x, τ)) + 81 / 2 * ((MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ))) ⊤
MeasureTheory.volume).toReal ^ 2 * lpsComparisonDistanceSq u v τ)
Fixed-time endpoint estimate for the relative convection, in the form used by the relative-energy assembly.