The elliptic identity ‖∇v‖² = ‖curl v‖² + ‖div v‖²

This file proves the elliptic identity 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 gradient energy ∫ ∑ᵢⱼ (∂ⱼvᵢ)² splits as ∫ ‖curl v‖² plus ∫ (div v)².

The proof expands both sides pointwise: ∑ᵢ (curl v)ᵢ² equals ∑ᵢⱼ (∂ⱼvᵢ)² - ∑ᵢⱼ ∂ⱼvᵢ ∂ᵢvⱼ, so the identity reduces to showing ∫ ∑ᵢⱼ ∂ⱼvᵢ ∂ᵢvⱼ = ∫ (∑ⱼ ∂ⱼvⱼ)². This cross-term identity is proved by two integrations by parts (moving ∂ⱼ off vᵢ and ∂ᵢ back onto vⱼ), with the symmetry of the second derivative used in between to commute the mixed partial ∂ⱼ∂ᵢvⱼ to ∂ᵢ∂ⱼvⱼ.

noncomputable def CIV.curlVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The curl of a time-independent vector field v : Vec3 → Vec3, with components (∂₂v₃ - ∂₃v₂, ∂₃v₁ - ∂₁v₃, ∂₁v₂ - ∂₂v₁).

Equations

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

theorem CIV.curlVec_apply_eq_curlComp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : curlVec v x = ![curlComp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => v z.1) 0 (x, t), curlComp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => v z.1) 1 (x, t), curlComp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => v z.1) 2 (x, t)]

On a time slice, curlVec agrees with the spatial part of the curlComp.

Regularity helpers

theorem CIV.contDiff_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x i

The i-th component of a smooth vector field is smooth.

theorem CIV.contDiff_fderiv_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i j : Fin 3) : ContDiff ℝ ↑⊤ fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => v z i) y) (CKN.basisVec j)

The derivative of the i-th component of a smooth vector field in a fixed direction is again smooth.

theorem CIV.continuous_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i : Fin 3) : Continuous fun (x : CKN.Foundation.Parabolic.Vec3) => v x i

v · i is continuous.

theorem CIV.continuous_fderiv_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i j : Fin 3) : Continuous fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec j)

fderiv ℝ (v · i) · (basisVec j) is continuous for a smooth vector field.

theorem CIV.continuous_fderiv_fderiv_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i j k : Fin 3) : Continuous fun (x : CKN.Foundation.Parabolic.Vec3) => (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)

The second derivative ∂ₖ∂ⱼvᵢ is continuous for a smooth vector field.

theorem CIV.hasCompactSupport_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hsupp : HasCompactSupport v) (i : Fin 3) : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => v x i

v · i has compact support.

theorem CIV.hasCompactSupport_fderiv_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hsupp : HasCompactSupport v) (i j : Fin 3) : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec j)

fderiv ℝ (v · i) · (basisVec j) has compact support.

theorem CIV.hasCompactSupport_fderiv_fderiv_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hsupp : HasCompactSupport v) (i j k : Fin 3) : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => (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)

The second derivative ∂ₖ∂ⱼvᵢ has compact support.

theorem CIV.differentiableAt_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x

v · i is differentiable everywhere.

theorem CIV.differentiableAt_fderiv_comp (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (i j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => v z i) y) (CKN.basisVec j)) x

fderiv ℝ (v · i) · (basisVec j) is differentiable everywhere.

theorem CIV.integrable_mul_of_continuous_of_hasCompactSupport {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : Continuous f) (hg : Continuous g) (hsupp : HasCompactSupport f) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) MeasureTheory.volume

A product of two continuous functions, one of them compactly supported, is integrable.

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

(∂ⱼvᵢ)² is integrable.

theorem CIV.integral_sum_sum_eq (f : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ) (hf : ∀ (i j : Fin 3), MeasureTheory.Integrable (f i j) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, f i j x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), f i j x

Pushing a finite double integral of a sum inside, or pulling it back out.

Symmetry of the second derivative

theorem CIV.fderiv_fderiv_comp_symm (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiff ℝ (↑⊤) G) (a b : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ G y) (CKN.basisVec a)) x) (CKN.basisVec b) = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ G y) (CKN.basisVec b)) x) (CKN.basisVec a)

Mixed partial derivatives of a smooth scalar function on Vec3 commute.

The cross-term identity

theorem CIV.integral_fderiv_mul_fderiv_symm (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hsupp : HasCompactSupport v) (hv : ContDiff ℝ (↑⊤) v) (i j : Fin 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec j) * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec i) = ∫ (x : CKN.Foundation.Parabolic.Vec3), (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec i) * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec j)

For a compactly supported smooth vector field, ∫ ∂ⱼvᵢ ∂ᵢvⱼ = ∫ ∂ᵢvᵢ ∂ⱼvⱼ. This is the key cancellation lemma for the elliptic identity: two integrations by parts, moving ∂ⱼ off vᵢ and ∂ᵢ back onto vⱼ, with the symmetry of the second derivative used in between to commute ∂ⱼ∂ᵢvⱼ to ∂ᵢ∂ⱼvⱼ.

theorem CIV.integral_cross_term_eq_sq_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, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec j) * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec i) = ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec j)) ^ 2

The double-sum cross-term identity: ∫ ∑ᵢⱼ ∂ⱼvᵢ ∂ᵢvⱼ = ∫ (∑ⱼ ∂ⱼvⱼ)².

The elliptic identity

theorem CIV.integral_sq_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, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec j) ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, curlVec v x i ^ 2) + ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec j)) ^ 2

The elliptic identity ‖∇v‖² = ‖curl v‖² + ‖div v‖² for a smooth compactly supported vector field on ℝ³.