Geometry of rescaled past cylinders

Every fixed bounded past cylinder lies in the rescaled source domain once the scale is sufficiently small (prop:blowup-limit).

def ESS.blowupSuitableDomain (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The rescaled preimage of the cylinder where local suitability is known.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.blowupCylinder_subset_domain (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 / 2) (htime : r ^ 2 * -a < 3 / 4) : CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo a 0 ⊆ blowupDomain x₀ t₀ r

A spatial and temporal scale bound places a fixed bounded past cylinder inside the rescaled original domain.

theorem ESS.blowupCylinder_eventually_subset_domain (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)) : ∀ᶠ (k : ℕ) in Filter.atTop, CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo a 0 ⊆ blowupDomain x₀ t₀ (r k)

Every fixed bounded past cylinder eventually lies in the source domain along any positive sequence of scales tending to zero.

theorem ESS.blowupCylinder_subset_suitableDomain (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) : CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo a 0 ⊆ blowupSuitableDomain x₀ t₀ r

The smaller spatial scale bound places a fixed cylinder in the region where the original solution is suitable.

theorem ESS.blowupSpatialBall_eventually_subset_inner (x₀ : CKN.Foundation.Parabolic.Vec3) (S : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : ∀ᶠ (k : ℕ) in Filter.atTop, CKN.Foundation.Parabolic.vec3Ball x₀ (r k * S) ⊆ CKN.euclideanBall 0 (3 / 4)

Shrinking balls centered over the closed half-ball eventually lie in the smaller source ball.

theorem ESS.blowupPastBox_subset_pastCylinder (R a : ℝ) (hR : 0 < R) (ha : a < 0) : ∃ (S : ℝ), 0 < S ∧ CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0 ⊆ CKN.Foundation.Parabolic.parabolicCylinder 0 0 S

Every bounded open past box fits inside a larger CKN past cylinder.