The gradient bound of eq:aniso:closure:elliptic

This file proves the first of the two elliptic bounds eq:aniso:closure:elliptic of Regularity of asymptotically axisymmetric solutions to the 3D Navier–Stokes equations with analytic forcing, arXiv:2609.20803, in the form in which the closure argument lem:aniso:closure uses it.

Let U be an open set, v : Vec3 → Vec3 smooth and divergence free on U, and χ a smooth cutoff whose support is a compact subset of U. The product χ • v is then smooth and compactly supported on all of ℝ³, so the elliptic identity integral_sq_fderiv_eq_curl_add_div applies to it: ∫ |∇(χ v)|² = ∫ |curl (χ v)|² + ∫ (div (χ v))². Expanding curl (χ v) = χ curl v + ∇χ × v and div (χ v) = ∇χ · v (the term χ div v vanishes on U, and everything vanishes off tsupport χ) and using |∇χ × v|² ≤ |∇χ|² |v|² and (∇χ · v)² ≤ |∇χ|² |v|² gives

∫ |∇(χ v)|² ≤ 2 ∫ χ² |curl v|² + 3 Mu² ∫ |∇χ|²,

where Mu bounds |v| wherever ∇χ ≠ 0. The first term on the right is the quantity Y t = ‖χ ω(·, t)‖² of lem:aniso:closure with ω = curl u; integral_cutoff_sq_curl_eq_curlComp records that shape in terms of the ambient curl curlComp of a space–time field.

The second elliptic bound of eq:aniso:closure:elliptic, the ∇²b estimate, is not proved here.

Vanishing off the support of the cutoff

Smoothness and support of a cutoff times a locally smooth field

theorem CIV.contDiff_smul_of_contDiffOn (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (U : Set CKN.Foundation.Parabolic.Vec3) (hU : IsOpen U) (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hsupp : tsupport χ ⊆ U) (hv : ContDiffOn ℝ (↑⊤) v U) : (ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => χ x • v x) ∧ HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => χ x • v x

A smooth compactly supported cutoff χ whose support sits inside an open set U turns a field v that is smooth only on U into a globally smooth, compactly supported field χ • v.

Continuity and integrability of the cutoff quantities

The Cauchy–Schwarz inequality in three components

The gradient bound

theorem CIV.integral_sq_fderiv_smul_le (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (U : Set CKN.Foundation.Parabolic.Vec3) (Mu : ℝ) (hU : IsOpen U) (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hsupp : tsupport χ ⊆ U) (hv : ContDiffOn ℝ (↑⊤) v U) (hdiv : ∀ x ∈ U, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec j) = 0) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), gradVec χ x ≠ 0 → ∑ i : Fin 3, v x i ^ 2 ≤ Mu ^ 2) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (χ y • v y) i) x) (CKN.basisVec j) ^ 2 ≤ (2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * ∑ i : Fin 3, curlVec v x i ^ 2) + 3 * Mu ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, gradVec χ x i ^ 2

The first inequality of eq:aniso:closure:elliptic: for a field v that is smooth and divergence free on an open set U and a smooth cutoff χ supported in U, with |v| ≤ Mu wherever ∇χ ≠ 0,

∫ |∇(χ v)|² ≤ 2 ∫ χ² |curl v|² + 3 Mu² ∫ |∇χ|².

In lem:aniso:closure the field v is the time slice of the velocity, so that ∫ χ² |curl v|² is the enstrophy Y t, and the last term is the constant C.

The enstrophy shape Y t = ‖χ ω(·, t)‖²

theorem CIV.integral_cutoff_sq_curl_eq_curlComp (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * ∑ i : Fin 3, curlVec v x i ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * ∑ i : Fin 3, curlComp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => v z.1) i (x, t) ^ 2

The quantity ∫ χ² |curl v|² of integral_sq_fderiv_smul_le, written with the ambient curl curlComp of the space–time field whose time slice is v. This is the enstrophy Y t = ‖χ ω(·, t)‖² of lem:aniso:closure.