Suitability on a fixed rescaled cylinder

The original suitable solution restricts and rescales to every fixed bounded past cylinder once the scale is small enough (prop:blowup-limit).

theorem ESS.blowupFields_eq_rescale_on_cylinder (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 → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r ρ a : ℝ) (hx₀ : CKN.Foundation.Parabolic.vec3EuclideanNorm x₀ ≤ 1 / 2) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : 0 < r) (hspace : r * ρ < 1 / 4) (htime : r ^ 2 * -a < 3 / 4) : Set.EqOn (blowupVelocity x₀ t₀ r u) (parabolicRescaleVelocity x₀ t₀ r u) (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo a 0) ∧ Set.EqOn (blowupGradient x₀ t₀ r Du) (parabolicRescaleGradient x₀ t₀ r Du) (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo a 0) ∧ Set.EqOn (blowupPressure x₀ t₀ r p) (parabolicRescalePressure x₀ t₀ r p) (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo a 0)

On each sufficiently small fixed cylinder, the zero-extended fields agree pointwise with the ordinary rescalings used for suitability.

theorem ESS.blowupRescale_suitable_on_cylinder (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 → ℝ) (hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r ρ a : ℝ) (hx₀ : CKN.Foundation.Parabolic.vec3EuclideanNorm x₀ ≤ 1 / 2) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : 0 < r) (hρ : 0 < ρ) (ha : a < 0) (hspace : r * ρ < 1 / 4) (htime : r ^ 2 * -a < 3 / 4) : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo a 0) 3 (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) (parabolicRescalePressure x₀ t₀ r p) 0

Navier--Stokes rescaling preserves suitability on a fixed past cylinder inside the rescaled source region.

theorem ESS.blowupRescale_eventually_suitable_on_cylinder (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 → ℝ) (hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ ρ a : ℝ) (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)) (hρ : 0 < ρ) (ha : a < 0) : ∀ᶠ (k : ℕ) in Filter.atTop, CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo a 0) 3 (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) (parabolicRescalePressure x₀ t₀ (r k) p) 0

The ordinary rescalings form a tail of suitable solutions on each fixed bounded past cylinder.