The public statement CIV.Main.regularAnnulus

This module proves the statement CIV.regularAnnulus (lem:aniso:annulus). The annulus assembly CIV.exists_annulus_bound_wholeBall_conditional_on_serrin takes two inputs beyond the standing data: the classical form of the equations, supplied by the weak-to-classical bridge CIV.isClassicalSolutionOn_of_suitable, and Serrin's interior derivative estimate CIV.Main.serrinInteriorEstimates.

theorem CIV.Main.regularAnnulus (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) (R₁ R₀ : ℝ) (hR : 0 ≤ R₁ ∧ R₁ < R₀ ∧ R₀ < 1) : ∃ (Rm : ℝ) (Rp : ℝ) (t₀ : ℝ), R₁ < Rm ∧ Rm < Rp ∧ Rp < R₀ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ (∃ (M : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ M) ∧ ∀ Rstar ∈ Set.Ioo Rm Rp, ∃ (CΓ : ℝ), ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ CΓ

The public statement of the regular-annulus lemma lem:aniso:annulus: between any two radii R₁ < R₀ < 1 there is an annulus and a final time interval on which the derivatives of u of order at most two are bounded, and on every smaller ball the circulation is bounded.