Whole-space div–curl estimates for smooth fields

The higher order estimate in lem:local-div-curl is obtained by applying the compactly supported smooth div–curl identity to each ordered derivative.

theorem ESS.localDivCurlSmooth_wordDeriv_spatialDeriv {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 3)) (j : Fin 3) : CKN.wordDeriv α (CKN.spatialDeriv f j) = CKN.spatialDeriv (CKN.wordDeriv α f) j

theorem ESS.localDivCurlSmooth_wordDeriv_sum (α : List (Fin 3)) {f : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (f i)) : (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f i x) = fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, CKN.wordDeriv α (f i) x

def ESS.localDivCurlSmoothTopWords (m : ℕ) : Finset (List (Fin 3))

Spatial derivative words of the highest order in the div–curl estimate.

Equations

• ESS.localDivCurlSmoothTopWords m = {α ∈ CKN.sobolevWords (m + 1) | α.length = m + 1}

def ESS.localDivCurlSmoothTopPairs (m : ℕ) : Finset (List (Fin 3) × Fin 3)

Highest-order derivative words paired with a spatial coordinate.

Equations

• ESS.localDivCurlSmoothTopPairs m = {α ∈ CKN.sobolevWords m | α.length = m}.product Finset.univ

noncomputable def ESS.localDivCurlSmoothDiv (V : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The divergence of a vector field given by its components.

Equations

• ESS.localDivCurlSmoothDiv V x = ∑ i : Fin 3, CKN.spatialDeriv (V i) i x

noncomputable def ESS.localDivCurlSmoothCurl (V : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) : CKN.Foundation.Parabolic.Vec3 → ℝ

A component of the curl of a vector field.

Equations

• ESS.localDivCurlSmoothCurl V k x = CKN.spatialDeriv (V (k + 2)) (k + 1) x - CKN.spatialDeriv (V (k + 1)) (k + 2) x

theorem ESS.divCurl_smooth_whole (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (V : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3), ContDiff ℝ (↑⊤) (V i)) → (∀ (i : Fin 3), HasCompactSupport (V i)) → (∑ i : Fin 3, CKN.sobolevNormSqOn (m + 1) Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α (V i)) ≤ C * (((CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, CKN.spatialDeriv (V i) i x) + ∑ k : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv (V (k + 2)) (k + 1) x - CKN.spatialDeriv (V (k + 1)) (k + 2) x) + ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α (V i))

Whole-space higher order div–curl estimate for compactly supported smooth fields (lem:local-div-curl).