The relative energy inequality #
For a finite-energy weak solution u with pressure in space-time L⁵ and a
finite-energy weak solution v in L^{10/3} satisfying the energy inequality,
the squared L² distance E(t) = ‖v(t) - u(t)‖₂² obeys
E(t) ≤ C ∫₀ᵗ ‖u(τ)‖₅⁵ E(τ) dτ at almost every time. This is the zero-start
energy comparison of lem:pv-serrin-uniqueness.
theorem
ESS.serrin_relative_slice_bound_ae
{T : ℝ}
{a b : 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 b v Dv pv)
(hu5 :
MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
{K : ℝ}
(hK :
∀ {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)
:
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, τ) k * ∑ j : Fin 3, (v (x, τ) j - u (x, τ) j) * (Dv (x, τ) k j - Du (x, τ) k j) ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, ∑ j : Fin 3, (Dv (x, τ) k j - Du (x, τ) k j) ^ 2) + K * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, τ)) (ENNReal.ofReal 5)
MeasureTheory.volume).toReal ^ 5 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, (v (x, τ) k - u (x, τ) k) ^ 2
At almost every time, the slice difference obeys the fixed-time relative convection bound.
theorem
ESS.serrin_relative_energy_inequality
{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)
(hu5 :
MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hv103 :
MeasureTheory.MemLp v (ENNReal.ofReal (10 / 3))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hvE :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * v (x, t) k ≤ (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k) - 2 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv q k j * Dv q k j)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, (v (x, t) k - u (x, t) k) ^ 2 ≤ C * ∫ (τ : ℝ) in 0..t, (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, τ)) (ENNReal.ofReal 5)
MeasureTheory.volume).toReal ^ 5 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, (v (x, τ) k - u (x, τ) k) ^ 2
The relative energy inequality at almost every time.