The Hessian half of eq:aniso:closure:elliptic

This file proves the second elliptic bound of eq:aniso:closure:elliptic, the estimate the gradient bound integral_sq_fderiv_smul_le leaves open: for a field v smooth and divergence free on an open set U and a cutoff χ supported in U,

∫ |∇²(χ v)|² ≤ 4 ∫ χ² |∇ curl v|² + 24 N² ∫ |∇χ|² + 24 N² ∫ |∇²χ|²,

where N bounds the first-order jet |v|² + |∇v|² of v on the support of ∇χ. The first term on the right is the enstrophy dissipation M t of lem:aniso:closure.

The proof applies the second-order identity integral_sq_fderiv_fderiv_eq_curl_add_div to the globally smooth compactly supported field χ v, which splits ∫ |∇²(χv)|² as ∫ |∇ curl (χv)|² + ∫ |∇ div (χv)|², and then expands each half by the Leibniz rule:

• curl (χ v) = χ curl v + ∇χ × v, so one more derivative produces four terms, three of which carry a derivative of χ and are therefore supported where the jet bound applies;
• div (χ v) = ∇χ · v on U, since v is divergence free there, so one more derivative produces two terms, both carrying a derivative of χ.

The cross-product terms are controlled by sum_sq_cross3_le, and the dot-product term by the Lagrange identity.

Regularity of the curl on the smoothness set

theorem CIV.contDiffOn_fderiv_scalar_apply {G : CKN.Foundation.Parabolic.Vec3 → ℝ} {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hG : ContDiffOn ℝ (↑⊤) G U) (k : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ G x) (CKN.basisVec k)) U

A coordinate derivative of a scalar smooth on an open set is smooth there.

theorem CIV.contDiffOn_curlVec_comp {V : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hV : ContDiffOn ℝ (↑⊤) V U) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (y : CKN.Foundation.Parabolic.Vec3) => curlVec V y i) U

A component of the curl of a field smooth on an open set is smooth there.

One derivative of the cross-product term

One derivative of the curl and the divergence of a cutoff product

Elementary sum inequalities

The pointwise bound on one derivative of the curl

The pointwise bound on one derivative of the divergence

Integrability of the cutoff-weighted curl dissipation

theorem CIV.integrable_cutoff_sq_sum_sq_fderiv_curlVec (w : CKN.Foundation.Parabolic.Vec3 → ℝ) (V : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (U : Set CKN.Foundation.Parabolic.Vec3) (hU : IsOpen U) (hw : ContDiff ℝ (↑⊤) w) (hws : HasCompactSupport w) (hsupp : tsupport w ⊆ U) (hV : ContDiffOn ℝ (↑⊤) V U) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => w x ^ 2 * ∑ i : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => curlVec V y i) x) (CKN.basisVec k) ^ 2) MeasureTheory.volume

χ² |∇ curl v|² is integrable when χ is a cutoff supported inside the smoothness set of v. This is the enstrophy dissipation of lem:aniso:closure.

The Hessian bound

theorem CIV.integral_sq_fderiv_fderiv_smul_le (w : CKN.Foundation.Parabolic.Vec3 → ℝ) (V : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (U : Set CKN.Foundation.Parabolic.Vec3) (N : ℝ) (hU : IsOpen U) (hw : ContDiff ℝ (↑⊤) w) (hws : HasCompactSupport w) (hsupp : tsupport w ⊆ 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) (hjet : ∀ x ∈ tsupport (gradVec w), ∑ i : Fin 3, V x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => V y i) x) (CKN.basisVec j) ^ 2 ≤ N ^ 2) : ∫ (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) => (w z • V z) i) y) (CKN.basisVec j)) x) (CKN.basisVec k) ^ 2 ≤ ((4 * ∫ (x : CKN.Foundation.Parabolic.Vec3), w x ^ 2 * ∑ i : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => curlVec V y i) x) (CKN.basisVec k) ^ 2) + 24 * N ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, gradVec w x i ^ 2) + 24 * N ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => gradVec w y i) x) (CKN.basisVec j) ^ 2

The Hessian half of eq:aniso:closure:elliptic. For a field v smooth and divergence free on an open set U, a cutoff χ smooth and compactly supported inside U, and N bounding the first-order jet of v on the support of ∇χ,

∫ |∇²(χ v)|² ≤ 4 ∫ χ² |∇ curl v|² + 24 N² ∫ |∇χ|² + 24 N² ∫ |∇²χ|².

It is the second-order identity integral_sq_fderiv_fderiv_eq_curl_add_div applied to χ v, followed by the Leibniz expansions of curl (χ v) and div (χ v).