Suitability of the blow-up limit

The rescaled source solutions are suitable on each fixed bounded past cylinder from some index on; with the local convergences of velocity, gradient, and pressure, thm:stability of the CKN manuscript makes the blow-up limit suitable there (prop:blowup-limit, the suitability step).

theorem ESS.blowupLimitAssembly_lintegral_sq_le_of_Lthree (g : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (Ω' : Set CKN.Foundation.Parabolic.Vec3) (M : ENNReal) (h3 : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (g x)) 3 MeasureTheory.volume ≤ M) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in Ω', ‖g x‖ₑ ^ 2 ≤ (M * MeasureTheory.volume Ω' ^ (1 / 6)) ^ 2

A global L³ slice bound gives a local L² slice bound by Hölder's inequality.

theorem ESS.blowupLimitAssembly_limit_suitable {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 : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hpmeas : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL2 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hpLp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) (hS2 : ∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0) (hS3 : ∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0) (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)) {um : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hum : Measurable um) (hu_um : u =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))] um) (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (hWmeas : Measurable W) (htrace : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, ⟨t, ht⟩)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (Mt : ℝ) (hsourceW : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) 3 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm ((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator (fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t)) x)) 3 MeasureTheory.volume ≤ ENNReal.ofReal Mt) (Dm : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hDmEq : goodPointDomain.indicator Dm =ᵐ[MeasureTheory.volume] goodPointDomain.indicator Du) (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hDU : ∀ (Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)), IsCompact Q → Q ⊆ Set.univ ×ˢ Set.Iio 0 → MeasureTheory.MemLp DU 2 (MeasureTheory.volume.restrict Q)) (hconvU : ∀ (R : ℝ), 0 < R → ∀ a < 0, Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupVelocity x₀ t₀ (r k) u z - U z) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)) (hconvD : ∀ (Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)), IsCompact Q → Q ⊆ Set.univ ×ˢ Set.Iio 0 → ∀ (i j : Fin 3) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict Q) → Filter.Tendsto (fun (k : ℕ) => ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Q, blowupGradient x₀ t₀ (r k) Dm z i j * w z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Q, DU z i j * w z))) (hconvP : ∀ (R : ℝ), 0 < R → ∀ a < 0, Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupPressure x₀ t₀ (r k) p z - q z) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo a 0) 3 U DU q 0

The blow-up limit is a suitable weak solution on every bounded past cylinder, by thm:stability of the CKN manuscript applied to a tail of the rescaled source solutions.