The public statement CIV.Main.axisymmetricTheorem

This module proves the statement CIV.axisymmetricTheorem (thm:aniso:main). The proof is the printed one: prop:aniso:small at ρ = 1/2 (CIV.Main.meridionalSmallness) gives eq:aniso:closure:small with ρ₀ = 1/2, and the closure lemma lem:aniso:closure, applied to the rotation-averaged triple (u, π_bar, 𝒫 f) whose force is axisymmetric (CIV.boundedNearOrigin_of_meridionalSmallness_averaged), makes (0,0) a regular point.

theorem CIV.Main.axisymmetricTheorem (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) : BoundedNearOrigin u

The public statement of thm:aniso:main: an axisymmetric suitable weak solution on the unit cylinder, smooth there, with a force satisfying eq:interior:force:c-two and the anisotropic bounds eq:aniso:bounds, is regular at the origin.