Assembly of the regular-annulus lemma

lem:aniso:annulus is the paper's regular-annulus lemma: from a suitable weak solution smooth on compact subsets of Q with a C²-bounded force, and radii R₁ < R₀ < 1, it produces a strictly smaller annulus and a time t₀ on which u, ∇u, ∇²u are bounded, and a circulation bound on every sub-radius. It has three ingredients: the choice of the annulus via the null Hausdorff measure of the singular set (exists_annulus_bound_of_timeZeroSingularSetNull), the circulation bound from an order-0 velocity bound (forall_Rstar_exists_circulation_bound_of_annulus_bound), and the interior derivative estimate for the Navier–Stokes system (Serrin, Section 4, m = 1). The *_conditional_on_serrin statements take the last as an explicit hypothesis hserrin, as step_annulus_derivative_bounds does; CIV.Main.regularAnnulus discharges it with CIV.Main.serrinInteriorEstimates. In this file the circulation bound is restricted to the annulus Rm < |x| < Rstar that forall_Rstar_exists_circulation_bound_of_annulus_bound delivers; exists_annulus_bound_wholeBall_conditional_on_serrin gives it on the full ball B(Rstar), as stated in the manuscript.

theorem CIV.exists_derivative_bound_conditional_on_serrin (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) (hMf : ForceC2Bounded f) (R₁ R₀ : ℝ) (hR₁ : 0 ≤ R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 1) (hserrin : ∀ (Rm Rp t₀ Mu : ℝ), 0 ≤ Rm → Rm < Rp → Rp ≤ 1 → t₀ ∈ Set.Ioo (-1) 0 → (∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) → ∀ (Rm' Rp' t₀' : ℝ), Rm < Rm' → Rm' < Rp' → Rp' < Rp → t₀ < t₀' → t₀' < 0 → ∃ (K : ℝ), ∀ (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)| ≤ K) : ∃ (Rm : ℝ) (Rp : ℝ) (t₀ : ℝ) (K : ℝ), R₁ < Rm ∧ Rm < Rp ∧ Rp < R₀ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ ∀ (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)| ≤ K

theorem CIV.exists_circulation_bound_conditional_on_serrin (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) (hMf : ForceC2Bounded f) (R₁ R₀ : ℝ) (hR₁ : 0 ≤ R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 1) (hserrin : ∀ (Rm Rp t₀ Mu : ℝ), 0 ≤ Rm → Rm < Rp → Rp ≤ 1 → t₀ ∈ Set.Ioo (-1) 0 → (∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) → ∀ (Rm' Rp' t₀' : ℝ), Rm < Rm' → Rm' < Rp' → Rp' < Rp → t₀ < t₀' → t₀' < 0 → ∃ (K : ℝ), ∀ (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)| ≤ K) : ∃ (Rm : ℝ) (Rp : ℝ) (t₀ : ℝ), R₁ < Rm ∧ Rm < Rp ∧ Rp < R₀ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ ∀ Rstar ∈ Set.Ioo Rm Rp, ∃ (CΓ : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rstar → ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ CΓ

theorem CIV.exists_annulus_bound_conditional_on_serrin (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) (hMf : ForceC2Bounded f) (R₁ R₀ : ℝ) (hR₁ : 0 ≤ R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 1) (hserrin : ∀ (Rm Rp t₀ Mu : ℝ), 0 ≤ Rm → Rm < Rp → Rp ≤ 1 → t₀ ∈ Set.Ioo (-1) 0 → (∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) → ∀ (Rm' Rp' t₀' : ℝ), Rm < Rm' → Rm' < Rp' → Rp' < Rp → t₀ < t₀' → t₀' < 0 → ∃ (K : ℝ), ∀ (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)| ≤ K) : ∃ (Rm : ℝ) (Rp : ℝ) (t₀ : ℝ), R₁ < Rm ∧ Rm < Rp ∧ Rp < R₀ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ (∃ (K : ℝ), ∀ (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)| ≤ K) ∧ ∀ Rstar ∈ Set.Ioo Rm Rp, ∃ (CΓ : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rstar → ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ CΓ

theorem CIV.circulation_bound_at_representative_radius_conditional_on_serrin (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) (hMf : ForceC2Bounded f) (R₁ R₀ : ℝ) (hR₁ : 0 ≤ R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 1) (hserrin : ∀ (Rm Rp t₀ Mu : ℝ), 0 ≤ Rm → Rm < Rp → Rp ≤ 1 → t₀ ∈ Set.Ioo (-1) 0 → (∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) → ∀ (Rm' Rp' t₀' : ℝ), Rm < Rm' → Rm' < Rp' → Rp' < Rp → t₀ < t₀' → t₀' < 0 → ∃ (K : ℝ), ∀ (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)| ≤ K) : ∃ (Rm : ℝ) (Rp : ℝ) (t₀ : ℝ) (Rstar : ℝ) (CΓ : ℝ), R₁ < Rm ∧ Rm < Rstar ∧ Rstar < Rp ∧ Rp < R₀ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rstar → ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ CΓ