Spatial propagation of vorticity vanishing #
This is the closedness step of the continuation argument in the proof of
thm:ess-local (spatial unique continuation): if the weak
vorticity vanishes near (x', t) and x' is within 1/8 of x, then it
vanishes near (x, t), provided the solution has bounded velocity on the unit
past cylinder with top (x, t + 1/8). The vorticity chart of
thm:vorticity-regularity supplies a regular representative, and unique
continuation (thm:uc, lem:flat-from-vanishing) is applied at every top time
near t.
theorem
ESS.essLocal_vorticityZero_propagate
{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 / 8) 1) ⊆ CKN.spaceTimeSet Set.univ J)
(hV :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.parabolicCylinder x (t + 1 / 8) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (V z) ≤ M)
(x' : CKN.Foundation.Parabolic.Vec3)
(hx' : CKN.Foundation.Parabolic.vec3EuclideanNorm (x' - x) < 1 / 8)
(r : ℝ)
(hr : 0 < r)
(hzero :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x' r) (Set.Ioo (t - r ^ 2) (t + r ^ 2))), weakVorticity DV z = 0)
:
∃ (r' : ℝ),
0 < r' ∧ ∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r') (Set.Ioo (t - r' ^ 2) (t + r' ^ 2))), weakVorticity DV z = 0
Vanishing of the weak vorticity near (x', t) propagates to a
neighborhood of (x, t) when |x' - x| < 1/8 and the velocity is bounded on
the unit past cylinder with top (x, t + 1/8).