Blowup Rescale Agreement

Agreement identities for the endpoint rescaling construction.

theorem ESS.blowupFields_eventually_eq_rescale_on_pastBox (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (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 : ℝ) : ∀ᶠ (k : ℕ) in Filter.atTop, ∀ z ∈ CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0, blowupVelocity x₀ t₀ (r k) u z = parabolicRescaleVelocity x₀ t₀ (r k) u z ∧ blowupPressure x₀ t₀ (r k) p z = parabolicRescalePressure x₀ t₀ (r k) p z

On each fixed past cylinder, zero extension agrees eventually with the ordinary rescalings used in the suitable-solution statement.

theorem ESS.blowupFields_eventually_eLpNorm_eq_rescale (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (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 : ℝ) : ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupVelocity x₀ t₀ (r k) u z)) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) = MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ (r k) u z)) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (blowupPressure x₀ t₀ (r k) p) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) = MeasureTheory.eLpNorm (parabolicRescalePressure x₀ t₀ (r k) p) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))

The eventual pointwise agreement transfers local velocity and pressure seminorms between zero extension and ordinary rescaling.