The public statement CIV.Main.mainTheorem

This module proves the statement CIV.mainTheorem (thm:main). The proof is the printed one: interior analyticity and the identity theorem make u axisymmetric on the unit cylinder (CIV.isAxisymmetricOn_unitCylinder_of_forceSpatiallyAnalytic), so the bounds eq:interior:mean:bounds on the angular mean are the bounds eq:aniso:bounds on u (CIV.anisotropicBounds_of_isAxisymmetricOn), and thm:aniso:main (CIV.Main.axisymmetricTheorem) makes (0,0) a regular point.

theorem CIV.Main.mainTheorem (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) (h : ℝ) (hh : 0 < h ∧ h < 1 / 2) (hMf : ForceC2Bounded f) (hfa : ForceSpatiallyAnalytic f) (C : ℝ) (hC : 0 < C) (hbounds : AnisotropicBounds C h (angularMean u)) (hcore : ∀ t ∈ Set.Ioo (-1) 0, ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) : IsAxisymmetricOn u unitCylinder ∧ BoundedNearOrigin u

The public statement of thm:main: under analytic forcing, the anisotropic bounds on the angular mean and an axisymmetric core at every time, the solution is axisymmetric on the unit cylinder and regular at the origin.