The rotation-averaged system and the regularity of axisymmetric solutions

For an axisymmetric suitable weak solution on Q, smooth there, averaging the momentum equation over the rotations about the axis leaves the velocity terms unchanged and replaces the pressure and the force by their angular means π_bar and f_bar = 𝒫 f (proof of thm:main). The pair (u, π_bar) is again suitable with the axisymmetric force f_bar: the classical equations give ∇π_bar - ∇π = f_bar - f on Q, so this is a smooth change of gauge. The closure lemma lem:aniso:closure applied to the averaged triple then gives regularity at the origin from the smallness eq:aniso:closure:small at one radius, with no symmetry assumed on the force; this is the proof of thm:aniso:main from prop:aniso:small.

theorem CIV.isSuitableWeakSolution_angularMean {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) (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) : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du (angularMeanScalar p) (angularMean f)

The averaged system is suitable: for an axisymmetric suitable weak solution on Q whose velocity, pressure and force are smooth there, (u, π_bar) is a suitable weak solution with the force 𝒫 f, with the same weak gradient.

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

thm:aniso:main from the smallness at one radius: an axisymmetric suitable weak solution on Q, smooth there, with a force satisfying eq:interior:force:c-two (no symmetry of the force is assumed) and lim_{t↑0} (-t) G_{ρ₀}(t) = 0 for some ρ₀ ∈ (0, 1), is regular at the origin. The closure lemma is applied to the averaged triple (u, π_bar, 𝒫 f).