Initial-time ball bound for the swirl coefficient from smoothness alone

The three theorems below supply the initial-time ball bound Mi required by CIV.swirl_bound_of_annulus_bound / CIV.swirl_bound_ball_of_annulus_bound (eq:aniso:closure:w) from smoothness of the classical solution alone. The key observation is that u(·, t₀) 1 is continuous on the closed ball closure (vec3Ball 0 Rstar) ⊆ vec3Ball 0 1 (Rstar < 1), hence bounded there by the extreme value theorem — exactly the template CIV.Reduction.AnalyticInductionBaseCase.exists_bound_of_contDiffOn_zero already uses for a scalar field.

This completes the reduction of CIV.swirl_bound_ball to a decay bound |u_θ| ≤ C_η (−t)^{−η} from nothing but a classical solution and a plain order-0 annulus bound.

theorem CIV.exists_abs_apply_one_le_of_contDiffOn_ball {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {Rstar tη : ℝ} (hRpos : 0 < Rstar) (hR1 : Rstar < 1) (htη : tη ∈ Set.Ioo (-1) 0) : ∃ (Mi : ℝ), 0 ≤ Mi ∧ ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, |u (x, tη) 1| ≤ Mi

theorem CIV.swirl_bound_ball_of_annulus_bound_and_contDiffOn (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (Mf : ℝ) (hMf : ∀ z ∈ unitCylinder, |f z 1| ≤ Mf) {Rlo Rhi t₀ M Rstar : ℝ} (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ M) (hR : 0 < Rstar ∧ Rstar < 1) (hRlo : Rlo < Rstar) (hRhi : Rstar < Rhi) (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {η : ℝ} (hη : 0 < η) (hG : ∀ t ∈ Set.Ioo t₀ 0, ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar → |radialQuotient u (meridional x₁ x₃, t)| ≤ η / -t) : ∃ (Mi : ℝ), 0 ≤ Mi ∧ ∀ t ∈ Set.Ioo t₀ 0, ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, x 0 ≠ 0 ∨ x 1 ≠ 0 → (-t) ^ η * |swirlCoeffAt u (x, t)| ≤ (-t₀) ^ η * max M Mi + (-t₀) ^ η * Mf * (t - t₀)

theorem CIV.exists_swirlCoeffAt_le_of_annulus_bound (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (Mf : ℝ) (hMf : ∀ z ∈ unitCylinder, |f z 1| ≤ Mf) {Rlo Rhi t₀ M Rstar : ℝ} (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ M) (hR : 0 < Rstar ∧ Rstar < 1) (hRlo : Rlo < Rstar) (hRhi : Rstar < Rhi) (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {η : ℝ} (hη : 0 < η) (hG : ∀ t ∈ Set.Ioo t₀ 0, ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar → |radialQuotient u (meridional x₁ x₃, t)| ≤ η / -t) : ∃ (Cη : ℝ), 0 ≤ Cη ∧ ∀ t ∈ Set.Ioo t₀ 0, ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, x 0 ≠ 0 ∨ x 1 ≠ 0 → |swirlCoeffAt u (x, t)| ≤ Cη * (-t) ^ (-η)