The public statement CIV.Main.closureLemma

This module proves the statement CIV.closureLemma (lem:aniso:closure). The proof is CIV.boundedNearOrigin_of_meridionalSmallness: the regular annulus of CIV.Main.regularAnnulus, the energy inequality eq:aniso:closure:energy for the canonical ball cutoff with the suprema G and W fixed before the constant C_*, the choice η = 1/(16 C_*), the swirl bound eq:aniso:closure:w by the axis maximum principle, the Grönwall and L⁶ steps, and the Gustafson–Kang–Tsai criterion CIV.Main.gktCriterion.

theorem CIV.Main.closureLemma (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) (hfaxi : IsAxisymmetricOn f unitCylinder) (hMf : ForceC2Bounded f) (ρ₀ : ℝ) (hρ₀ : ρ₀ ∈ Set.Ioo 0 1) (hsmall : MeridionalSmallness ρ₀ u) : BoundedNearOrigin u

The public statement of the closure lemma lem:aniso:closure: for an axisymmetric suitable weak solution, smooth on the unit cylinder, with an axisymmetric force satisfying eq:interior:force:c-two, the smallness lim_{t↑0} (-t) G_{ρ₀}(t) = 0 of eq:aniso:closure:small for some ρ₀ ∈ (0, 1) makes (0,0) a regular point.