Helper lemmas for the contradiction dichotomy #
theorem
CIV.strictMono_comp_and_tendsto_zero_of_reindex
{t : ℕ → ℝ}
(ht_mono : StrictMono t)
(ht_tendsto : Filter.Tendsto t Filter.atTop (nhds 0))
{φ : ℕ → ℕ}
(hφ : StrictMono φ)
:
Dichotomy for prop:aniso:small's proof by contradiction #
theorem
CIV.exists_seq_three_terms_dichotomy
{ρ h C : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
(haxi : IsAxisymmetricOn u unitCylinder)
(hb : AnisotropicBounds C h u)
(hh : 0 < h)
(hρ : ρ ≤ 1)
(hnot : ¬MeridionalSmallness ρ u)
:
∃ (c₀ : ℝ),
0 < c₀ ∧ ∃ (t : ℕ → ℝ) (x₁ : ℕ → ℝ) (x₃ : ℕ → ℝ),
(∀ (n : ℕ), 0 ≤ x₁ n) ∧ StrictMono t ∧ Filter.Tendsto t Filter.atTop (nhds 0) ∧ (∀ (n : ℕ), meridional (x₁ n) (x₃ n) ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) ∧ (∀ (n : ℕ), t n ∈ Set.Ioo (-1) 0) ∧ (∀ (n : ℕ),
c₀ < -t n * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0
(meridional (x₁ n) (x₃ n), t n)| + |radialQuotient u (meridional (x₁ n) (x₃ n), t n)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (x₁ n) (x₃ n), t n)|)) ∧ ((∃ (A : ℝ), ∀ (n : ℕ), x₁ n / √(-t n) ≤ A) ∨ Filter.Tendsto (fun (n : ℕ) => x₁ n / √(-t n)) Filter.atTop Filter.atTop)
The reindexed contradiction data and finite-axis/receding-axis dichotomy for
prop:aniso:small's proof by contradiction (its common set-up): from a failure of
MeridionalSmallness, a sequence of points and times realizing the
eq:aniso:G-lower-bound, refined along a subsequence on which the radial coordinate divided by the
zoom scale λ n = √(−t n) is either bounded (Step 2, finite axis) or tends to infinity (Step 3,
receding axis).