The stretching-term bounds of lem:aniso:closure

This file proves two of the estimates that go into the tested vortex-stretching term of lem:aniso:closure, from Regularity of asymptotically axisymmetric solutions to the 3D Navier–Stokes equations with analytic forcing, arXiv:2609.20803: the unlabeled prose bound, right after eq:aniso:closure:stretch, of the first three terms and the ∂_z u_r term by C G Y, and the labeled eq:aniso:closure:angular:bound.

The plane-to-ball transfer

CIV.Identities.PlaneTransfer proves the cylindrical identities stretching_meridional and gradient_sq_meridional on the meridional plane {x₂ = 0}, and transfers rotation-invariant scalars (the Frobenius norm of ∇u, the Euclidean norm of curl u, the vortex-stretching scalar) to the whole ball via exists_rotZ_meridional: every x is rotZ φ (meridional r x₃) for a unique r ≥ 0. The uniqueness is made explicit here: r is forced to be polarR x = √(x₀² + x₁²) and x₃ is forced to be x 2 (polarR_eq_of_rotZ_meridional), so the representative point of x is the explicit, globally continuous map x ↦ meridional (polarR x) (x 2) — continuous everywhere (including on the axis, where it is the identity), though not differentiable there.

This lets us read the cylindrical quantities of eq:aniso:closure:stretch at the representative of a general point x, and bound them there: stretchGTerm u x t packages the first three terms of the stretching sum and the ∂_z u_r term, and stretchAngularSwirl u x t packages the angular term's swirl factor u_θ · (ω_r/r). Both are built from radialQuotient, which is already known continuous across the axis (continuousOn_radialQuotient_plane), so both are continuous on the whole open unit ball, and the pointwise bounds of abs_stretchGTerm_le and abs_two_mul_stretchAngularSwirl_mul_curlComp_one_le integrate directly against χ² to the two inequalities stretchGTerm_integral_le and stretchAngularTerm_integral_abs_le.

The remaining piece of eq:aniso:closure:stretch, the mixed term (∂_r u_z) ω_r ω_z, is bounded by integration by parts in the z-direction (eq:aniso:closure:mixed, CIV.integral_cutoff_sq_stretchMixedTerm_eq), which needs differentiability off the axis rather than the continuity of the representative map used here. CIV.energy_inequality_of_mixed_term_bound sums this file's two bounds with the mixed term into eq:aniso:closure:energy.

The explicit meridional representative

noncomputable def CIV.polarR (x : CKN.Foundation.Parabolic.Vec3) : ℝ

The distance from x to the vertical axis, √(x₀² + x₁²). This is the modulus used by exists_rotZ_meridional, made explicit: continuous on all of Vec3 (though not differentiable on the axis).

Equations

• CIV.polarR x = √(x 0 ^ 2 + x 1 ^ 2)

theorem CIV.polarR_nonneg (x : CKN.Foundation.Parabolic.Vec3) : 0 ≤ polarR x

theorem CIV.continuous_polarR : Continuous polarR

theorem CIV.polarR_eq_of_rotZ_meridional {x : CKN.Foundation.Parabolic.Vec3} {φ r x₃ : ℝ} (hr : 0 ≤ r) (hxeq : x = rotZ φ (meridional r x₃)) : polarR x = r ∧ x 2 = x₃

Any witness (φ, r, x₃) of exists_rotZ_meridional x with r ≥ 0 has r = polarR x and x₃ = x 2: the polar radius and height of x are forced by the rotated-meridional relation.

theorem CIV.exists_rotZ_polarR (x : CKN.Foundation.Parabolic.Vec3) : ∃ (φ : ℝ), x = rotZ φ (meridional (polarR x) (x 2))

Every point is the image, under some rotation about the axis, of its own explicit meridional representative meridional (polarR x) (x 2).

theorem CIV.vec3EuclideanNorm_polarR_rep (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm (meridional (polarR x) (x 2)) = CKN.Foundation.Parabolic.vec3EuclideanNorm x

The meridional representative of x has the same Euclidean norm as x: a direct algebraic identity, polarR x ^ 2 + x 2 ^ 2 = x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2, not needing rotation invariance.

theorem CIV.rep_mem_vec3Ball {x : CKN.Foundation.Parabolic.Vec3} {ρ : ℝ} (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) : meridional (polarR x) (x 2) ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ

The meridional representative of a point of an open ball about the origin is again in that same ball: the argument is radius-agnostic, since it rests only on vec3EuclideanNorm_polarR_rep.

theorem CIV.polarRRep_mapsTo : Set.MapsTo (fun (x : CKN.Foundation.Parabolic.Vec3) => (polarR x, x 2)) (CKN.Foundation.Parabolic.vec3Ball 0 1) {y : ℝ × ℝ | y.1 ^ 2 + y.2 ^ 2 < 1}

The representative pair (polarR x, x 2) lands in the open disk {y₁² + y₂² < 1} when x is in the open unit ball.

The two invariant scalars, read at the explicit representative

theorem CIV.curlSq_eq_polarR {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn v unitCylinder) (hv : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z) unitCylinder) {x : CKN.Foundation.Parabolic.Vec3} {t : ℝ} (hz : (x, t) ∈ unitCylinder) : ∑ i : Fin 3, curlComp v i (x, t) ^ 2 = ∑ i : Fin 3, curlComp v i (meridional (polarR x) (x 2), t) ^ 2

The Euclidean curl-squared of an axisymmetric field agrees at every point with its value at the point's explicit meridional representative.

theorem CIV.gradientSq_eq_polarR {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn v unitCylinder) (hv : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z) unitCylinder) {x : CKN.Foundation.Parabolic.Vec3} {t : ℝ} (hz : (x, t) ∈ unitCylinder) : ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => v w i) j (x, t) ^ 2 = ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => v w i) j (meridional (polarR x) (x 2), t) ^ 2

The Frobenius gradient-squared of an axisymmetric field agrees at every point with its value at the point's explicit meridional representative.

Smoothness of the vorticity field

theorem CIV.contDiffOn_vorticityField {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityField u z) unitCylinder

The Cartesian vorticity of a smooth velocity is smooth.

The four-term part of eq:aniso:closure:stretch

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

The first three terms and the ∂_z u_r term of eq:aniso:closure:stretch, read at the meridional representative of x: (∂_r u_r) ω_r² + (u_r/r) ω_θ² + (∂_z u_z) ω_z² + (∂_z u_r) ω_r ω_z, all evaluated at meridional (polarR x) (x 2). On the meridional plane itself (x 1 = 0, x 0 ≥ 0) the representative is x, and this is literally the manuscript's expression.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.abs_stretchGTerm_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {t G ρ : ℝ} (hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) (hG : ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → meridionalQuantity u (meridional x₁ x₃, t) ≤ G) (hGnn : 0 ≤ G) {x : CKN.Foundation.Parabolic.Vec3} (hxρ : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (ht : t ∈ Set.Ioo (-1) 0) : |stretchGTerm u x t| ≤ 2 * G * ∑ i : Fin 3, curlComp u i (x, t) ^ 2

The pointwise bound behind eq:aniso:closure:stretch's four-term estimate. stretchGTerm is bounded, at every point of the ball B(ρ) (for ρ ≤ 1), by 2 G times the local enstrophy density, whenever the four cylindrical quantities of meridionalQuantity are bounded by G at every meridional-plane point of B(ρ). Each of the four coefficients of stretchGTerm is one of those four quantities (meridionalQuantity's definition), and the two mixed products are split by 2|ab| ≤ a² + b².

Continuity, and the integral form of the four-term estimate

theorem CIV.continuousOn_stretchGTerm {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) : ContinuousOn (fun (x : CKN.Foundation.Parabolic.Vec3) => stretchGTerm u x t) (CKN.Foundation.Parabolic.vec3Ball 0 1)

The four-term stretching part is continuous on the unit ball, since it is built from the already-continuous slices of u and of the curl, composed with the continuous representative map, plus the one piece built from radialQuotient, continuous across the axis by continuousOn_radialQuotient_plane.

theorem CIV.stretchGTerm_integral_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) {ρ : ℝ} (hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t G : ℝ} (ht : t ∈ Set.Ioo (-1) 0) (hG : ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → meridionalQuantity u (meridional x₁ x₃, t) ≤ G) (hGnn : 0 ≤ G) : ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchGTerm u x t ≤ 2 * G * cutoffEnstrophy χ u t

The four-term estimate, integrated. The four-term part of the vortex-stretching integrand, integrated against χ², is bounded by 2 G times the cutoff enstrophy Y t, whenever χ's support sits inside a ball B(ρ) ⊆ B(1) on which the four cylindrical quantities of meridionalQuantity are bounded by G: the radius MeridionalSmallness ρ actually delivers.

The angular term of eq:aniso:closure:angular:bound

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

The swirl factor of the angular term eq:aniso:closure:angular:bound: u_θ · (ω_r / r), read at the meridional representative of x.

Equations

• CIV.stretchAngularSwirl u x t = u (CIV.meridional (CIV.polarR x) (x 2), t) 1 * CIV.radialQuotient (CIV.vorticityField u) (CIV.meridional (CIV.polarR x) (x 2), t)

theorem CIV.abs_two_mul_stretchAngularSwirl_mul_curlComp_one_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {t W ρ : ℝ} (hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) (hW : ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → |u (meridional x₁ x₃, t) 1| ≤ W) {x : CKN.Foundation.Parabolic.Vec3} (hxρ : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (ht : t ∈ Set.Ioo (-1) 0) : |2 * stretchAngularSwirl u x t * curlComp u 1 (meridional (polarR x) (x 2), t)| ≤ 1 / 4 * ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => vorticityField u w i) j (x, t) ^ 2 + 4 * W ^ 2 * ∑ i : Fin 3, curlComp u i (x, t) ^ 2

The pointwise bound behind eq:aniso:closure:angular:bound. Twice the product of the angular swirl factor with ω_θ is bounded, at every point of the ball B(ρ) (for ρ ≤ 1), by a quarter of the local dissipation density plus 4 W² times the local enstrophy density, whenever |u_θ| ≤ W at every meridional-plane point of B(ρ). The proof is the AM–GM bound 2 W A B ≤ ¼ A² + 4 W² B² with A = ω_r/r, B = ω_θ, followed by A² ≤ |∇ω|² (sq_radialQuotient_le_gradientSq, applied to ω, dropping the nonnegative ω_θ²/r² summand) and B² ≤ |ω|².

Continuity, and the integral form of the angular term

theorem CIV.continuousOn_stretchAngularSwirl {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) : ContinuousOn (fun (x : CKN.Foundation.Parabolic.Vec3) => stretchAngularSwirl u x t) (CKN.Foundation.Parabolic.vec3Ball 0 1)

The angular swirl factor is continuous on the unit ball: it is built from the continuous slice of u and from radialQuotient (vorticityField u), continuous across the axis by continuousOn_radialQuotient_plane applied to the smooth axisymmetric field vorticityField u.

theorem CIV.stretchAngularTerm_integral_abs_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) {ρ : ℝ} (hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t W : ℝ} (ht : t ∈ Set.Ioo (-1) 0) (hW : ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → |u (meridional x₁ x₃, t) 1| ≤ W) : |∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * (2 * stretchAngularSwirl u x t * curlComp u 1 (meridional (polarR x) (x 2), t))| ≤ 1 / 4 * cutoffEnstrophyDissipation χ u t + 4 * W ^ 2 * cutoffEnstrophy χ u t

eq:aniso:closure:angular:bound, integrated. Twice the product of the angular swirl factor with ω_θ, integrated against χ² in absolute value, is bounded by a quarter of the cutoff dissipation M t plus 4 W² times the cutoff enstrophy Y t, whenever χ's support sits inside a ball B(ρ) ⊆ B(1) on which |u_θ| ≤ W: the radius CIV.swirl_bound_ball actually delivers.