The second-order elliptic identity ‖∇²v‖² = ‖∇ curl v‖² + ‖∇ div v‖²

This file proves the second-order form of eq:aniso:closure:elliptic of Regularity of asymptotically axisymmetric solutions to the 3D Navier–Stokes equations with analytic forcing, arXiv:2609.20803: for a smooth, compactly supported vector field v : Vec3 → Vec3, the Hessian energy ∫ ∑ᵢⱼₖ (∂ₖ∂ⱼvᵢ)² splits as ∫ ‖∇ curl v‖² plus ∫ ‖∇ div v‖².

The proof differentiates the first-order identity integral_sq_fderiv_eq_curl_add_div of CIV.Analysis.DivCurl. Applying it to the field ∂ₖv = partialVec v k, which is again smooth with compact support, and using that ∂ₖ commutes with both curl and div (curlVec_partialVec, div_partialVec), gives for each direction k

∫ ‖∇ ∂ₖv‖² = ∫ ‖∂ₖ curl v‖² + ∫ (∂ₖ div v)².

Summing the three identities and using sum_sq_partialVec_eq to recognise the left-hand side as the Hessian energy of v gives the statement. No new integration by parts is performed here: the one that matters is already inside the first-order identity.

Regularity of the curl

theorem CIV.contDiff_curlVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) : ContDiff ℝ (↑⊤) (curlVec v)

The curl of a smooth vector field is smooth.

theorem CIV.hasCompactSupport_curlVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hsupp : HasCompactSupport v) : HasCompactSupport (curlVec v)

The curl of a compactly supported vector field has compact support.

theorem CIV.integrable_sum_sq_fderiv_curlVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (hsupp : HasCompactSupport v) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => curlVec v y i) x) (CKN.basisVec k) ^ 2) MeasureTheory.volume

The gradient energy of the curl is integrable for a smooth compactly supported field.

Regularity of the divergence

The integrability of the three energies, direction by direction

The second-order identity

theorem CIV.integral_sq_fderiv_fderiv_eq_curl_add_div (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (hsupp : HasCompactSupport v) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => v z i) y) (CKN.basisVec j)) x) (CKN.basisVec k) ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => curlVec v y i) x) (CKN.basisVec k) ^ 2) + ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => v z j) y) (CKN.basisVec j)) x) (CKN.basisVec k) ^ 2

The second-order elliptic identity ‖∇²v‖² = ‖∇ curl v‖² + ‖∇ div v‖² for a smooth compactly supported vector field on ℝ³. It is the first-order identity integral_sq_fderiv_eq_curl_add_div applied to each directional derivative ∂ₖv and summed over the three directions.