Blowup Compactness Source

Compactness of the rescaled fields in the endpoint regularity argument.

theorem ESS.blowupRescale_strong_Lthree_to_time_zero_of_local_Ltwo (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0) (hu : MeasureTheory.AEStronglyMeasurable (goodPointDomain.indicator u) MeasureTheory.volume) (Mᵤ : ENNReal) (hMᵤ : Mᵤ < ⊤) (hsourceU : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => goodPointDomain.indicator u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (x, s))) 3 MeasureTheory.volume ≤ Mᵤ) (hp₁ : MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) (Mₚ : ENNReal) (hMₚ : Mₚ < ⊤) (hsourceP : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) (3 / 2) MeasureTheory.volume ≤ Mₚ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2) - p₁ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t) - p₁ (x, t)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hlocal : ∀ b < 0, Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => parabolicRescaleVelocity x₀ t₀ (r k) u z - v z) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a b))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => parabolicRescaleVelocity x₀ t₀ (r k) u z - v z) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

The source slice and pressure bounds upgrade local strong L² convergence of rescaled velocities to strong L³ convergence on every bounded cylinder ending at time zero.