Matching a strong solution with a Leray–Hopf solution

A strong solution that agrees almost everywhere with a Leray–Hopf solution on a slab has the same gradient there, and its slice at the end time agrees with the Leray–Hopf slice in the weak sense (lem:lps-continuation).

theorem ESS.lps_weak_gradient_ae_eq {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} {G G' : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hf : CKN.HasWeakGradientOn Set.univ f G) (hg : CKN.HasWeakGradientOn Set.univ g G') (hfg : f =ᵐ[MeasureTheory.volume] g) (hG : MeasureTheory.MemLp G 2 MeasureTheory.volume) (hG' : MeasureTheory.MemLp G' 2 MeasureTheory.volume) : G =ᵐ[MeasureTheory.volume] G'

Weak gradients of almost everywhere equal square-integrable functions agree almost everywhere.

theorem ESS.lps_strong_gradient_ae_eq_slab {T t₀ t₁ : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hLH : CKN.IsLerayHopfSolution T a u Du) (hU : IsLpsStrongSolution t₀ t₁ U DU p) (ht₀ : 0 ≤ t₀) (ht₁ : t₁ ≤ T) (hae : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u) : DU =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] Du

A strong solution that agrees with a Leray–Hopf solution on a slab has the same gradient there (lem:lps-continuation).

theorem ESS.lps_weak_slice_eq {T t₀ t₁ : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hLH : CKN.IsLerayHopfSolution T a u Du) (hU : IsLpsStrongSolution t₀ t₁ U DU p) (ht₀ : 0 ≤ t₀) (ht₁ : t₁ ≤ T) (hae : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u) (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₁) i * w x i = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t₁) i * w x i

The end-time slice of a strong solution that agrees with a Leray–Hopf solution on a slab agrees with the Leray–Hopf slice in the weak sense (lem:lps-continuation).