A uniform H¹ bound along strong continuations

A strong solution that agrees on (t₀, t₁), t₁ ≤ T, with a Leray–Hopf solution of finite Serrin norm has H¹ norm at time t₁ bounded independently of t₁ by the H¹ estimate (lem:lps-H1-estimate, lem:lps-continuation).

theorem ESS.lps_h1_norm_le_of_parts {t₀ t₁ : ℝ} {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 → ℝ} {e f : ℝ} (hU : IsLpsStrongSolution t₀ t₁ U DU p) (hL2 : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₁) i ^ 2 ≤ e) (hH1 : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, DU (x, t₁) i j ^ 2 ≤ f) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₁) i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, DU (x, t₁) i j ^ 2 ≤ e + f

The H¹ norm at time t₁ is at most the sum of the L² norm and the gradient norm, each controlled by its value at the initial time.

theorem ESS.lps_strong_l2_le_initial {t₀ t₁ : ℝ} {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 → ℝ} (hU : IsLpsStrongSolution t₀ t₁ U DU p) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₁) i ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₀) i ^ 2

The L² norm of a strong solution does not increase (prop:lps-local-strong).

theorem ESS.lps_mixed_finite_transfer {T t₀ t₁ s : ℝ} {u U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (ht₀ : 0 ≤ t₀) (ht₁ : t₁ ≤ T) (hae : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u) (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 : ℝ) in Set.Ioo t₀ t₁, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤

Transfer of the finite mixed Serrin norm from a Leray–Hopf solution to a strong solution agreeing with it on the time interval.

theorem ESS.lps_mixed_endpoint_transfer {T t₀ t₁ : ℝ} {u U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (ht₀ : 0 ≤ t₀) (ht₁ : t₁ ≤ T) (hae : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u) (hmix : ∫⁻ (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 < ⊤) : ∫⁻ (t : ℝ) in Set.Ioo t₀ t₁, essSup (fun (x : CKN.Foundation.Parabolic.Vec3) => ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t)))) MeasureTheory.volume ^ 2 < ⊤

Transfer of the endpoint Serrin norm from a Leray–Hopf solution to a strong solution agreeing with it on the time interval.

theorem ESS.lps_continuation_bound {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} (hLH : CKN.IsLerayHopfSolution T a u Du) (hSerrin : (∃ (s : ℝ), 3 < s ∧ ∫⁻ (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 : ℝ) in Set.Ioo 0 T, essSup (fun (x : CKN.Foundation.Parabolic.Vec3) => ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))) MeasureTheory.volume ^ 2 < ⊤) (ht₀ : 0 ≤ t₀) : ∃ (S : ℝ), ∀ {t₁ : ℝ} {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 → ℝ}, IsLpsStrongSolution t₀ t₁ U DU p → t₁ ≤ T → ((fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) → ((fun (x : CKN.Foundation.Parabolic.Vec3) => DU (x, t₀)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t₀)) → U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₁) i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, DU (x, t₁) i j ^ 2 ≤ S

A bound on the H¹ norm of every strong solution that agrees with a Leray–Hopf solution of finite Serrin norm on an initial time interval (lem:lps-H1-estimate, lem:lps-continuation).