Meridional Smallness Lemmas

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.MeridionalSmallness.mono {ρ ρ' : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : MeridionalSmallness ρ u) (hle : ρ' ≤ ρ) : MeridionalSmallness ρ' u

Monotonicity of MeridionalSmallness in the ball radius: if the condition holds for radius ρ, it holds for every smaller radius ρ'.

theorem CIV.meridionalQuantity_nonneg (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : 0 ≤ meridionalQuantity u z

The meridional quantity is nonnegative everywhere.

theorem CIV.not_meridionalSmallness_iff {ρ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} : ¬MeridionalSmallness ρ u ↔ ∃ (c₀ : ℝ), 0 < c₀ ∧ ∀ t₀ ∈ Set.Ioo (-1) 0, ∃ t ∈ Set.Ioo t₀ 0, ∃ (x₁ : ℝ) (x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ ∧ c₀ < -t * meridionalQuantity u (meridional x₁ x₃, t)

The negation of MeridionalSmallness ρ u is equivalent to the existence of a positive constant c₀ and sequences approaching the singular time at which the scaled quantity exceeds c₀. This is the unfolding of the logical negation eq:aniso:zoom:selected.

theorem CIV.exists_seq_of_not_meridionalSmallness {ρ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : ¬MeridionalSmallness ρ u) : ∃ (c₀ : ℝ), 0 < c₀ ∧ ∃ (t : ℕ → ℝ) (x₁ : ℕ → ℝ) (x₃ : ℕ → ℝ), StrictMono t ∧ (∀ (n : ℕ), t n ∈ Set.Ioo (-1) 0) ∧ Filter.Tendsto t Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), meridional (x₁ n) (x₃ n) ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ ∧ c₀ < -t n * meridionalQuantity u (meridional (x₁ n) (x₃ n), t n)

From the failure of MeridionalSmallness ρ u we can extract a positive constant c₀ and sequences t n → 0⁻, x₁ n, x₃ n such that the scaled meridional quantity remains bounded below by c₀.