Vorticity charts and spatial propagation of vanishing

On a unit past cylinder where a suitable solution has bounded velocity, thm:vorticity-regularity gives a regular vorticity representative. Unique continuation (thm:uc) applied at every top time near t then propagates vanishing of the weak vorticity near (x', t) to a space-time neighborhood of (x, t) whenever x' is close to x; this is the closedness step in the proof of thm:ess-local (spatial unique continuation).

theorem ESS.essLocal_le_of_ae_le_of_continuousOn {O : Set CKN.Foundation.Parabolic.ParabolicPoint} (hO : IsOpen O) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContinuousOn f O) {C : ℝ} (h : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict O, f z ≤ C) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ O → f z ≤ C

An essential upper bound of a function continuous on an open parabolic set holds at every point of that set.

theorem ESS.essLocal_ae_restrict_of_local {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) {P : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (h : ∀ z ∈ S, ∃ (N : Set CKN.Foundation.Parabolic.ParabolicPoint), IsOpen N ∧ z ∈ N ∧ ∀ᵐ (y : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict N, P y) : ∀ᵐ (y : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict S, P y

A property holding almost everywhere near every point of a parabolic set holds almost everywhere on that set.

theorem ESS.essLocal_convex_vec3Ball (c : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : Convex ℝ (CKN.Foundation.Parabolic.vec3Ball c r)

A Euclidean ball in Vec3 is convex.

theorem ESS.essLocal_vorticityChart {J : Set ℝ} {V : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DV : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (M : ℝ) (hM : 0 ≤ M) (hsws : CKN.IsSuitableWeakSolution Set.univ J 3 V DV pv 0) (x : CKN.Foundation.Parabolic.Vec3) (t₁ : ℝ) (hcl : closure (CKN.Foundation.Parabolic.parabolicCylinder x t₁ 1) ⊆ CKN.spaceTimeSet Set.univ J) (hV : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x t₁ 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (V z) ≤ M) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (ω : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dω : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2ω : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtω : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), ω =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x t₁ (1 / 2))] weakVorticity DV ∧ ContinuousOn ω (closure (CKN.Foundation.Parabolic.parabolicCylinder x t₁ (1 / 2))) ∧ CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x (1 / 2)) (Set.Ioo (t₁ - 1 / 4) t₁) ω Dω D2ω Dtω ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x t₁ (1 / 2), ‖ω z‖ₑ ^ 2 + ‖Dω z‖ₑ ^ 2 + ‖D2ω z‖ₑ ^ 2 + ‖Dtω z‖ₑ ^ 2 < ⊤ ∧ (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x t₁ (1 / 2)), (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtω z i - ∑ j : Fin 3, D2ω z i j j) ≤ C * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ω z) + √(CKN.spatialGradientSq ω Dω z))) ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x t₁ (1 / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ω z) ≤ C

thm:vorticity-regularity on a unit past cylinder of a suitable solution on a spatially global slab, with the gradient energy bound supplied by suitability.