Curl fields for the Leray data space

The cutoff construction in lem:J-weak-div uses compactly supported curls as divergence-free approximants.

noncomputable def CKN.curlVec3 (A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (x : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3

The curl of a smooth vector field, in the native three-dimensional coordinates.

Equations

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

def CKN.crossVec3 (u v : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3

The cross product on the native three-dimensional carrier.

Equations

• CKN.crossVec3 u v i = if i = 0 then u 1 * v 2 - u 2 * v 1 else if i = 1 then u 2 * v 0 - u 0 * v 2 else u 0 * v 1 - u 1 * v 0

theorem CKN.curlVec3_smul_scalar {η : Foundation.Parabolic.Vec3 → ℝ} {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hη : ContDiff ℝ (↑⊤) η) (hA : ContDiff ℝ (↑⊤) A) (x : Foundation.Parabolic.Vec3) : curlVec3 (fun (y : Foundation.Parabolic.Vec3) => η y • A y) x = η x • curlVec3 A x + crossVec3 (fun (i : Fin 3) => spatialDeriv η i x) (A x)

The product rule for the curl of a scalar multiple of a vector field.

theorem CKN.curlVec3_cutoff_error {η : Foundation.Parabolic.Vec3 → ℝ} {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hη : ContDiff ℝ (↑⊤) η) (hA : ContDiff ℝ (↑⊤) A) (x : Foundation.Parabolic.Vec3) : curlVec3 (fun (y : Foundation.Parabolic.Vec3) => η y • A y) x - curlVec3 A x = (η x - 1) • curlVec3 A x + crossVec3 (fun (i : Fin 3) => spatialDeriv η i x) (A x)

Splitting the cutoff curl error into the potential-gradient term and the tail of the original curl.

theorem CKN.curlVec3_hasCompactSupport {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hA : HasCompactSupport A) : HasCompactSupport (curlVec3 A)

The curl preserves compact support.

theorem CKN.cutoffCurl_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hη : HasCompactSupport η) : HasCompactSupport (curlVec3 fun (x : Foundation.Parabolic.Vec3) => η x • A x)

A curl obtained from a compactly supported scalar cutoff has compact support even when the underlying vector field does not.

theorem CKN.curlVec3_contDiff {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hA : ContDiff ℝ (↑⊤) A) : ContDiff ℝ (↑⊤) (curlVec3 A)

The curl of a smooth vector field is smooth.

theorem CKN.curlVec3_divergence_eq_zero {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hA : ContDiff ℝ (↑⊤) A) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => curlVec3 A y i) i x = 0

The divergence of the curl of a smooth vector field vanishes pointwise.

theorem CKN.smooth_cutoffCurl_divergence_eq_zero {η : Foundation.Parabolic.Vec3 → ℝ} {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hη : ContDiff ℝ (↑⊤) η) (hA : ContDiff ℝ (↑⊤) A) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => curlVec3 (fun (z : Foundation.Parabolic.Vec3) => η z • A z) y i) i x = 0

Multiplying a smooth potential by a smooth scalar cutoff and taking its curl gives a smooth divergence-free vector field.

theorem CKN.smooth_cutoffCurl_contDiff {η : Foundation.Parabolic.Vec3 → ℝ} {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hη : ContDiff ℝ (↑⊤) η) (hA : ContDiff ℝ (↑⊤) A) : ContDiff ℝ (↑⊤) (curlVec3 fun (x : Foundation.Parabolic.Vec3) => η x • A x)

The cutoff curl is smooth whenever the cutoff and potential are smooth.

theorem CKN.cutoffCurl_eLpNorm_sub_le {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hA : ContDiff ℝ (↑⊤) A) (hA2 : MeasureTheory.MemLp A 2 MeasureTheory.volume) (hcurl2 : MeasureTheory.MemLp (curlVec3 A) 2 MeasureTheory.volume) {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : MeasureTheory.eLpNorm ((curlVec3 fun (x : Foundation.Parabolic.Vec3) => canonicalBallCutoff 0 r R x • A x) - curlVec3 A) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm ((euclideanBall 0 r)ᶜ.indicator (curlVec3 A)) 2 MeasureTheory.volume + ‖64 / (R - r)‖ₑ * MeasureTheory.eLpNorm A 2 MeasureTheory.volume

Cutting off an L² vector potential approximates its curl in L². The first term is the curl tail and the second is the cutoff-gradient error.