Blowup Compactness Top

Compactness of the rescaled fields in the endpoint regularity argument.

theorem ESS.blowup_strong_Lthree_to_time_zero (A : Set CKN.Foundation.Parabolic.Vec3) (hA : MeasurableSet A) (hAfin : MeasureTheory.volume A < ⊤) (a : ℝ) (f : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (g : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hf : ∀ (k : ℕ), MeasureTheory.MemLp (f k) (10 / 3) ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a 0))) (hbound : ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (f k) (10 / 3) ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a 0)) ≤ B) (hlocal : ∀ b < 0, Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f k z - g z) 2 ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a b))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f k z - g z) 3 ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

Local strong L² convergence below time zero and a uniform L^(10/3) bound imply strong L³ convergence on a bounded cylinder with open top. This is the boundary-strip step of prop:blowup-limit.

theorem ESS.blowup_strong_Lthree_to_time_zero_eventually (A : Set CKN.Foundation.Parabolic.Vec3) (hA : MeasurableSet A) (hAfin : MeasureTheory.volume A < ⊤) (a : ℝ) (f : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (g : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hhigh : ∃ B < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.MemLp (f k) (10 / 3) ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (f k) (10 / 3) ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a 0)) ≤ B) (hlocal : ∀ b < 0, Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f k z - g z) 2 ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a b))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f k z - g z) 3 ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

The same strong-convergence upgrade applies when the common high-exponent bound starts only after a finite index.

theorem ESS.blowup_strong_Lthree_to_time_zero_parabolic (A : Set CKN.Foundation.Parabolic.Vec3) (hA : MeasurableSet A) (hAfin : MeasureTheory.volume A < ⊤) (a : ℝ) (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hhigh : ∃ B < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.MemLp (f k) (10 / 3) (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (f k) (10 / 3) (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a 0)) ≤ B) (hlocal : ∀ b < 0, Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f k z - g z) 2 (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a b))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f k z - g z) 3 (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

The open-top L³ upgrade stated with the parabolic volume used by the rescaled Navier–Stokes fields.