Tools for the terminal value of the vorticity

The curl of a smooth compactly supported spatial test, the weak curl identity on a time slice, the continuity of the vorticity pairing up to the top time, the slice form of an almost everywhere space-time identity, and the identification of a limit through an almost everywhere equal function (lem:vorticity-top-extension).

theorem ESS.vorticityTopZero_component_tsupport (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : (tsupport fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x i) ⊆ tsupport ψ

A component of a vector test is supported in the support of the test.

theorem ESS.vorticityTopZero_deriv_eq_zero {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport ψ) (i j : Fin 3) : CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j x = 0

The derivative of a component of a vector test vanishes off the support of the test.

theorem ESS.vorticityTopZero_curl_eq_zero {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport ψ) : spatialTestCurl ψ x = 0

The curl of a vector test vanishes off the support of the test.

theorem ESS.vorticityTopZero_integral_six {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3} {A B C D E F : CKN.Foundation.Parabolic.Vec3 → ℝ} (hA : MeasureTheory.Integrable A μ) (hB : MeasureTheory.Integrable B μ) (hC : MeasureTheory.Integrable C μ) (hD : MeasureTheory.Integrable D μ) (hE : MeasureTheory.Integrable E μ) (hF : MeasureTheory.Integrable F μ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), A x - B x + (C x - D x) + (E x - F x) ∂μ = ∫ (x : CKN.Foundation.Parabolic.Vec3), A x ∂μ - ∫ (x : CKN.Foundation.Parabolic.Vec3), B x ∂μ + (∫ (x : CKN.Foundation.Parabolic.Vec3), C x ∂μ - ∫ (x : CKN.Foundation.Parabolic.Vec3), D x ∂μ) + (∫ (x : CKN.Foundation.Parabolic.Vec3), E x ∂μ - ∫ (x : CKN.Foundation.Parabolic.Vec3), F x ∂μ)

The integral of a combination of six integrable functions.

theorem ESS.vorticityTopZero_slice_pairing {Ω' : Set CKN.Foundation.Parabolic.Vec3} (hfin : MeasureTheory.volume Ω' ≠ ⊤) {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω')) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict Ω')) (hw : ∀ (i : Fin 3), CKN.HasWeakGradientOn Ω' (fun (x : CKN.Vec 3) => u x i) fun (x : CKN.Vec 3) => Du x i) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφΩ : tsupport φ ⊆ Ω') : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialWeakVorticity Du x i * φ x i = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * spatialTestCurl φ x i

The weak curl identity on a spatial slice: pairing the curl of a weak gradient with a vector test is pairing the field with the curl of the test.

theorem ESS.vorticityTopZero_ae_rep {A : Set CKN.Foundation.Parabolic.Vec3} {B : Set ℝ} {ω : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hωae : ∀ (i : Fin 3), ω i =ᵐ[MeasureTheory.volume.restrict (A ×ˢ B)] fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => w z i) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφA : tsupport φ ⊆ A) : ∀ᵐ (t : ℝ), t ∈ B → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, ω k (x, t) * φ x k = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, w (x, t) k * φ x k

An almost everywhere space-time identity of the vorticity pairs identically with a test on almost every time slice.

theorem ESS.vorticityTopZero_limit_eq {f g : ℝ → ℝ} {a L : ℝ} (ha : a < 0) (hf : Filter.Tendsto f (nhdsWithin 0 (Set.Iio 0)) (nhds L)) (hg : Filter.Tendsto g (nhdsWithin 0 (Set.Iio 0)) (nhds 0)) (hfg : ∀ᵐ (t : ℝ), t ∈ Set.Ioo a 0 → f t = g t) : L = 0

A limit from negative times is determined by an almost everywhere equal function.

theorem ESS.vorticityTopZero_tendsto {x₁ : CKN.Foundation.Parabolic.Vec3} {r a C : ℝ} (ha : a < 0) {ω : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hωc : ∀ (i : Fin 3), ContinuousOn (ω i) ({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₁) ≤ r} ×ˢ Set.Icc a 0)) (hωb : ∀ (i : Fin 3), ∀ z ∈ {x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₁) ≤ r} ×ˢ Set.Icc a 0, |ω i z| ≤ C) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφ : Continuous φ) (hφc : HasCompactSupport φ) (hφB : tsupport φ ⊆ CKN.Foundation.Parabolic.vec3Ball x₁ r) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, ω k (x, t) * φ x k) (nhdsWithin 0 (Set.Iio 0)) (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, ω k (x, 0) * φ x k))

The pairing of a vorticity continuous up to the top time with a spatial test is continuous from below at the top time.