Assembly of the closure lemma lem:aniso:closure

The proof of lem:aniso:closure from its steps. A regular annulus R₋ < |x| < R₊ inside B(ρ₀) comes from lem:aniso:annulus with R₁ = 0, R₀ = ρ₀; the cutoff is the canonical ball cutoff between the radii ρ = (2R₋ + R₊)/3 and R_* = (R₋ + 2R₊)/3. The two suprema entering the energy inequality eq:aniso:closure:energy are fixed before the constant C_* is produced: G = meridionalG ρ₀ u (eq:aniso:G) and W = meridionalSwirlSup R_* u (eq:aniso:closure:w), both read on the meridional plane, which is all the stretching, angular and mixed-term estimates consume. Only then is η = 1/(16 C_*) chosen, t_η taken from eq:aniso:closure:small, the swirl bound eq:aniso:closure:w obtained by the axis maximum principle, and the Grönwall, L⁶ and Gustafson–Kang–Tsai steps run.

noncomputable def CIV.meridionalSwirlSup (R : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The swirl supremum W(t) = ‖u_θ(·, t)‖_{L^∞(B(R))} of eq:aniso:closure:w, read on the meridional plane, where the Cartesian component u₁ is the azimuthal velocity u_θ.

Equations

• CIV.meridionalSwirlSup R u t = sSup {a : ℝ | ∃ (x₁ : ℝ) (x₃ : ℝ), CIV.meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 R ∧ a = |u (CIV.meridional x₁ x₃, t) 1|}

theorem CIV.meridionalSwirlSup_nonneg (R : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) : 0 ≤ meridionalSwirlSup R u t

The swirl supremum is nonnegative.

theorem CIV.abs_apply_one_le_meridionalSwirlSup {R B t : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hB : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 R, |u (x, t) 1| ≤ B) {x₁ x₃ : ℝ} (hmem : meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 R) : |u (meridional x₁ x₃, t) 1| ≤ meridionalSwirlSup R u t

Every meridional value of |u_θ| in B(R) is at most the swirl supremum, once the values are bounded.

theorem CIV.meridionalSwirlSup_le {R B t : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hR : 0 < R) (hB : ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 R → |u (meridional x₁ x₃, t) 1| ≤ B) : meridionalSwirlSup R u t ≤ B

The swirl supremum is at most any bound on the meridional values of |u_θ| in B(R), for R > 0.

theorem CIV.le_mul_rpow_neg_of_weighted_le {tη t η a B Mf : ℝ} (hMf : 0 ≤ Mf) (ht : t ∈ Set.Ioo tη 0) (h : (-t) ^ η * a ≤ (-tη) ^ η * B + (-tη) ^ η * Mf * (t - tη)) : a ≤ (-tη) ^ η * (B + Mf * -tη) * (-t) ^ (-η)

The rearrangement of the weighted swirl bound of eq:aniso:closure:w: from (-t)^η a ≤ (-t_η)^η B + (-t_η)^η M_f (t - t_η) on (t_η, 0) one gets a ≤ C_η (-t)^{-η} with C_η = (-t_η)^η (B + M_f (-t_η)).

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

The closure lemma lem:aniso:closure. For an axisymmetric suitable weak solution, smooth on the unit cylinder, with an axisymmetric force satisfying eq:interior:force:c-two, the smallness lim_{t↑0} (-t) G_{ρ₀}(t) = 0 of eq:aniso:closure:small makes (0,0) a regular point.