Boundary data for the swirl bound from an annulus bound

The two theorems below supply the parabolic-boundary hypothesis hbdry of swirl_bound / swirl_bound_ball (eq:aniso:closure:w) from a plain order-0 bound on a space–time annulus that contains the sphere |x| = Rstar. The first lemma deduces the pointwise estimate |u (x, t) 1| ≤ M on the sphere from the annulus bound hbound using abs_apply_le_vec3EuclideanNorm. The two main theorems then instantiate swirl_bound / swirl_bound_ball with this hbdry, taking Mb := M and preserving Mi as given by hinit.

theorem CIV.hbdry_of_annulus_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {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) (hRlo : Rlo < Rstar) (hRhi : Rstar < Rhi) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm x = Rstar → ∀ t ∈ Set.Ioo t₀ 0, |u (x, t) 1| ≤ M

theorem CIV.swirl_bound_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) {Mi : ℝ} (hinit : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, |u (x, t₀) 1| ≤ Mi) (t : ℝ) : t ∈ Set.Ioo t₀ 0 → ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar → (-t) ^ η * |u (meridional x₁ x₃, t) 1| ≤ (-t₀) ^ η * max M Mi + (-t₀) ^ η * Mf * (t - t₀)

theorem CIV.swirl_bound_ball_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) {Mi : ℝ} (hinit : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, |u (x, t₀) 1| ≤ Mi) (t : ℝ) : 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₀)