Common relative-energy assembly for Leray–Hopf solutions

Once a branch supplies the cross identity, its explicit relative-convection integrability, and the fixed-time estimate, this theorem combines the distinguished solution's a.e. energy equality with the competitor's Leray–Hopf energy inequality and applies Gronwall.

theorem ESS.lps_comparison_time_weight_integrable {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 → ℝ} {m : ℝ → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T b v Dv pv) (hm : MeasureTheory.IntegrableOn m (Set.Ioo 0 T) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (t : ℝ) => m t * lpsComparisonDistanceSq u v t) (Set.Ioo 0 T) MeasureTheory.volume

Multiplication by an integrable time coefficient preserves integrability of the relative slice energy: the two Leray–Hopf slice energies bound that energy uniformly almost everywhere.

theorem ESS.lps_leray_hopf_relative_energy_zero_of_comparison_data {T K : ℝ} {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 → ℝ} {m : ℝ → ℝ} (hVLH : CKN.IsLerayHopfSolution T a v Dv) (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T a v Dv pv) (hK : 0 ≤ K) (hEnergyEquality : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = -2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Du z k j) (hRelativeCross : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = (-∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeConvection u v Du Dv z) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Dv z k j) (hSliceBound : ∀ᵐ (τ : ℝ) ∂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, τ)) + K * (m τ * lpsComparisonDistanceSq u v τ)) (hC : MeasureTheory.Integrable (lpsRelativeConvection u v Du Dv) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hm : MeasureTheory.IntegrableOn m (Set.Ioo 0 T) MeasureTheory.volume) (hmNonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ m t) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t = 0

Relative-energy and Gronwall conclusion from branch-specific comparison data. The energy equality remains an explicit hypothesis, supplied by lem:lps-energy-equality; the cross identity and convection integrability are the outputs of a branch's cross-testing limit.

theorem ESS.lps_leray_hopf_relative_energy_inequality_of_comparison_data {T K : ℝ} {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 → ℝ} {m : ℝ → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T a v Dv pv) (hEnergyEquality : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = -2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Du z k j) (hEnergyInequality : ∀ᵐ (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 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv z k j * Dv z k j) (hRelativeCross : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = (-∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeConvection u v Du Dv z) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Dv z k j) (hSliceBound : ∀ᵐ (τ : ℝ) ∂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, τ)) + K * (m τ * lpsComparisonDistanceSq u v τ)) (hC : MeasureTheory.Integrable (lpsRelativeConvection u v Du Dv) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hGradient : MeasureTheory.Integrable (lpsRelativeGradientSq Du Dv) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hmE : MeasureTheory.IntegrableOn (fun (t : ℝ) => m t * lpsComparisonDistanceSq u v t) (Set.Ioo 0 T) MeasureTheory.volume) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t ≤ 2 * K * ∫ (τ : ℝ) in 0..t, m τ * lpsComparisonDistanceSq u v τ

The same assembly stated as the comparison inequality before the final Gronwall conclusion.