Assembly

A positive-time restart may be chosen where both the good-slice conditions and the almost-every-time energy equality hold (lem:lps-good-times and lem:lps-energy-equality).

theorem ESS.lps_good_energy_time_in_interval {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 < ⊤) {δ : ℝ} (hδ : 0 < δ) (hδT : δ ≤ T) : ∃ t ∈ Set.Ioo 0 δ, IsLpsGoodTime u Du 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 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Du q k j

A positive-time restart may be chosen where both the good-slice conditions and the almost-every-time energy equality hold (lem:lps-good-times and lem:lps-energy-equality).

theorem ESS.lps_local_restart_from_good_energy_time (hLocal : ∃ (c : ℝ), 0 < c ∧ ∀ (t₀ : ℝ) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3), IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) t₀ → ∃ (τ : ℝ), 0 < τ ∧ c * (1 + √(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2)).rpow (-4) ≤ τ ∧ ∃ (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 ∧ (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume] b ∧ Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, s) - b x) 2 MeasureTheory.volume) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds 0) ∧ (∀ (s t : ℝ), s ∈ Set.Icc t₀ (t₀ + τ) → t ∈ Set.Icc t₀ (t₀ + τ) → s ≤ t → (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i ^ 2) + 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, ∑ j : Fin 3, DU z i j ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, s) i ^ 2) ∧ CKN.IsLerayHopfSolution τ b (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => U (z.1, t₀ + z.2)) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => DU (z.1, t₀ + z.2) i) {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 < ⊤) {δ : ℝ} (hδ : 0 < δ) (hδT : δ ≤ T) : ∃ t₀ ∈ Set.Ioo 0 δ, (∫ (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 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Du q k j ∧ ∃ (τ : ℝ), 0 < τ ∧ (∃ (c : ℝ), 0 < c ∧ c * (1 + √(∫ (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)).rpow (-4) ≤ τ) ∧ ∃ (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 ∧ ((fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) ∧ Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, s) - u (x, t₀)) 2 MeasureTheory.volume) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds 0) ∧ (∀ (s t : ℝ), s ∈ Set.Icc t₀ (t₀ + τ) → t ∈ Set.Icc t₀ (t₀ + τ) → s ≤ t → (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i ^ 2) + 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, ∑ j : Fin 3, DU z i j ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, s) i ^ 2) ∧ CKN.IsLerayHopfSolution τ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => U (z.1, t₀ + z.2)) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => DU (z.1, t₀ + z.2) i

Start the local strong solution at a time where both the good-slice conditions and the Serrin energy identity hold. The local existence theorem is an input here so that the restart assembly is independent of its provider.