Assembly Global

Patch compatible smooth representatives from later-than-zero intervals into one representative on the whole positive-time slab (thm:lps).

@[reducible, inline]

abbrev ESS.lpsAssemblySlab (a b : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The open time slab over all of space.

Equations

• ESS.lpsAssemblySlab a b = CKN.spaceTimeSet Set.univ (Set.Ioo a b)

@[reducible, inline]

abbrev ESS.lpsAssemblyTopSlab (a b : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The time slab over all of space including its top time slice.

Equations

• ESS.lpsAssemblyTopSlab a b = CKN.spaceTimeSet Set.univ (Set.Ioc a b)

theorem ESS.lps_patch_smooth_representatives {T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (t : ℕ → ℝ) (htPos : ∀ (n : ℕ), 0 < t n) (htBase : t 0 < T / 2) (hCover : ∀ (s : ℝ), 0 < s → s < T / 2 → ∃ (n : ℕ), t n < s) (v : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hvEq : ∀ (n : ℕ), v n =ᵐ[MeasureTheory.volume.restrict (lpsAssemblySlab (t n) T)] u) (top : ℕ → ℝ) (hTop : ∀ (n : ℕ), T < top n) (hvSmooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v n (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (Set.univ ×ˢ Set.Ioc (t n) (top n))) : ∃ (uSmooth : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), uSmooth =ᵐ[MeasureTheory.volume.restrict (lpsAssemblySlab 0 T)] u ∧ ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => uSmooth (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (Set.univ ×ˢ Set.Ioc 0 T)

Patch compatible smooth representatives from later-than-zero intervals into one representative on the whole positive-time slab (thm:lps).

theorem ESS.lps_ladyzhenskaya_prodi_serrin_of_node_conclusions (hD5 : ∀ {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}, CKN.IsLerayHopfSolution T a u Du → (∃ (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 < ⊤ → (∀ᵐ (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 * ∫ (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) → ∀ t₀ ∈ Set.Ioo 0 T, 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 → ∃ (t₁ : ℝ), 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 → ℝ), 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₀)) ∧ U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))] u) (hD6 : ∀ {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}, CKN.IsLerayHopfSolution T a u Du → (∃ (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 < ⊤ → ∀ (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3), CKN.IsLerayHopfSolution T a v Dv → v =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u) (hD7 : ∀ {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 → ℝ}, IsLpsStrongSolution t₀ t₁ U DU p → ∃ (R : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), R =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] U ∧ ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => R z) (Set.univ ×ˢ Set.Ioc 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} (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 < ⊤) : (∀ (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3), CKN.IsLerayHopfSolution T a v Dv → v =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u) ∧ ∃ (uSmooth : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), uSmooth =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u ∧ ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => uSmooth z) (Set.univ ×ˢ Set.Ioc 0 T)

Assemble the exact thm:lps conclusion from the continuation, uniqueness, and smoothing conclusions for its source-facing nodes. The continuation input is the conclusion of lem:lps-continuation; it receives the a.e. energy identity from lem:lps-energy-equality and a time in the joint good and equality set.