Local tools for the exterior vorticity at the terminal face

Uniqueness of weak time derivatives, agreement of continuous representatives on overlapping half-cylinders, a countable family of half-cylinders covering the exterior region, and finite covers of bounded subsets of the exterior region (lem:vorticity-top-extension).

theorem ESS.vorticity_weakTime_unique {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {f g₁ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg₁ : MeasureTheory.IntegrableOn g₁ W MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ W MeasureTheory.volume) (h₁ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₁ y * ψ y) (h₂ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₂ y * ψ y) : ∀ᵐ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict W, g₁ y = g₂ y

Uniqueness of the weak time derivative.

theorem ESS.vorticityTop_agree {ω₁ ω₂ h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {c₁ c₂ : CKN.Foundation.Parabolic.Vec3 × ℝ} (hc₁ : ContinuousOn ω₁ ({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - c₁.1) ≤ 1 / 2} ×ˢ Set.Icc (c₁.2 - 1 / 4) c₁.2)) (hc₂ : ContinuousOn ω₂ ({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - c₂.1) ≤ 1 / 2} ×ˢ Set.Icc (c₂.2 - 1 / 4) c₂.2)) (hae₁ : ω₁ =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c₁.1 (1 / 2) ×ˢ Set.Ioo (c₁.2 - 1 / 4) c₁.2)] h) (hae₂ : ω₂ =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c₂.1 (1 / 2) ×ˢ Set.Ioo (c₂.2 - 1 / 4) c₂.2)] h) {x : CKN.Foundation.Parabolic.Vec3} {t : ℝ} (hx₁ : CKN.Foundation.Parabolic.vec3EuclideanNorm (x - c₁.1) < 1 / 2) (hx₂ : CKN.Foundation.Parabolic.vec3EuclideanNorm (x - c₂.1) < 1 / 2) (ht₁ : t ∈ Set.Ioc (c₁.2 - 1 / 4) c₁.2) (ht₂ : t ∈ Set.Ioc (c₂.2 - 1 / 4) c₂.2) : ω₁ (x, t) = ω₂ (x, t)

Two representatives, continuous on closed half-cylinders and almost everywhere equal to the same function on the open half-cylinders, agree at every common point below or on the tops.

theorem ESS.vorticityTop_centers (R₂ : ℝ) : ∃ (A₀ : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)), A₀.Countable ∧ (∀ c ∈ A₀, R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm c.1 ∧ c.2 ∈ Set.Ioo (-2) 0) ∧ ∀ z ∈ {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} ×ˢ Set.Ioo (-2) 0, ∃ c ∈ A₀, z ∈ CKN.Foundation.Parabolic.vec3Ball c.1 (1 / 2) ×ˢ Set.Ioo (c.2 - 1 / 4) c.2

A countable family of exterior half-cylinders with tops below zero covering the open exterior region.

theorem ESS.vorticityTop_finiteCover {R₂ : ℝ} (hR₂ : 0 < R₂) {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hS : S ⊆ {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} ×ˢ Set.Ioo (-2) 0) (hSb : Bornology.IsBounded S) : ∃ (F : Finset (CKN.Foundation.Parabolic.Vec3 × ℝ)), (∀ c ∈ F, R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm c.1 ∧ c.2 ∈ Set.Ioc (-2) 0) ∧ S ⊆ ⋃ c ∈ F, CKN.Foundation.Parabolic.vec3Ball c.1 (1 / 2) ×ˢ Set.Ioo (c.2 - 1 / 4) c.2

A bounded subset of the open exterior region is covered by finitely many exterior half-cylinders with tops in (-2, 0].

theorem ESS.vorticity_timePartial_off {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) : CKN.timePartial ψ z = 0

The time derivative of a test function vanishes off its support.

theorem ESS.vorticity_weakTime_restrict {W W' : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW' : W' ⊆ W) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W' → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', f y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', g y * ψ y

A weak time derivative restricts to smaller sets.

theorem ESS.vorticity_weakPartial_unique_of_ae {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {f₁ f₂ g₁ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {j : Fin 3} (hf : f₁ =ᵐ[MeasureTheory.volume.restrict W] f₂) (hg₁ : MeasureTheory.IntegrableOn g₁ W MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ W MeasureTheory.volume) (h₁ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₁ y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₁ y * ψ y) (h₂ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₂ y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₂ y * ψ y) : g₁ =ᵐ[MeasureTheory.volume.restrict W] g₂

Uniqueness of the weak spatial derivative of almost everywhere equal functions.

theorem ESS.vorticity_weakTime_unique_of_ae {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {f₁ f₂ g₁ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : f₁ =ᵐ[MeasureTheory.volume.restrict W] f₂) (hg₁ : MeasureTheory.IntegrableOn g₁ W MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ W MeasureTheory.volume) (h₁ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₁ y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₁ y * ψ y) (h₂ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₂ y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₂ y * ψ y) : g₁ =ᵐ[MeasureTheory.volume.restrict W] g₂

Uniqueness of the weak time derivative of almost everywhere equal functions.

theorem ESS.vorticityTop_localIdentity {D N : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f g f' g' : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (L : (CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hLoff : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ∀ z ∉ tsupport ψ, L ψ z = 0) (hf : f =ᵐ[MeasureTheory.volume.restrict (N ∩ D)] f') (hg : g =ᵐ[MeasureTheory.volume.restrict (N ∩ D)] g') (hid : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ N → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in N, f' y * L ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in N, g' y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ N → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * L ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y

A weak identity on a neighbourhood passes to a larger domain for tests supported in both, when the integrands agree almost everywhere on the intersection.

theorem ESS.vorticity_ineq_convert {Cb : ℝ} (hCb : 0 ≤ Cb) (w Dtw : CKN.Foundation.Parabolic.Vec3) (Dw : Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (h : ∀ (i : Fin 3), |Dtw i - ∑ j : Fin 3, D2w i j j| ≤ Cb * (∑ l : Fin 3, |w l| + ∑ a : Fin 3, ∑ b : Fin 3, |Dw a b|)) : (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw i - ∑ j : Fin 3, D2w i j j) ≤ 27 * Cb * (CKN.Foundation.Parabolic.vec3EuclideanNorm w + √(∑ i : Fin 3, ∑ j : Fin 3, Dw i j ^ 2))

The differential inequality of the vorticity from its componentwise form.

theorem ESS.vorticity_isBounded_of_parabolic {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (h : Bornology.IsBounded S) : Bornology.IsBounded S

A set bounded for the parabolic distance is bounded in Vec3 × ℝ.