The public statement CIV.Main.meridionalSmallness

This module proves the statement CIV.meridionalSmallness (prop:aniso:small). The proof is the zoom argument of Section sec:aniso:zoom. Assume eq:aniso:small fails at a radius ρ. The selection eq:aniso:zoom:selected and the finite/receding dichotomy (CIV.exists_seq_three_terms_dichotomy) give times t_n ↑ 0 and points (x₁ n, x₃ n). With the angle-averaged classical system and the circulation bound eq:aniso:zoom:circulation (CIV.exists_zoom_standing_data), each branch runs four steps:

• compactness;
• the limit equation;
• the comparison principle lem:aniso:comparison;
• the endpoint argument.

The last step contradicts the selection.

theorem CIV.Main.meridionalSmallness (q : ℝ) (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 → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (henergy : GlobalEnergyClass u Du p) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (h : ℝ) (hh : 0 < h ∧ h < 1 / 2) (hMf : ForceC2Bounded f) (C : ℝ) (hC : 0 < C) (hbounds : AnisotropicBounds C h u) (ρ : ℝ) : ρ ∈ Set.Ioo 0 1 → MeridionalSmallness ρ u

The public statement of prop:aniso:small: under the hypotheses of thm:aniso:main, for every 0 < ρ < 1, (-t) G_ρ(t) → 0 as t ↑ 0 (eq:aniso:small).