Vorticity vanishing on a regular slab #
On a unit-scale slab B_{ρ+1} × (-2, 2) where a suitable solution has bounded
velocity, vanishing of the weak vorticity on a small seed cylinder propagates
through the connected ball B_ρ at every time of (-1, 1). This is the
connectedness argument in the proof of thm:ess-local, with the relatively
closed step supplied by
essLocal_vorticityZero_propagate.
theorem
ESS.essLocal_slabVorticityZero
{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)
(hJ : Set.Ioo (-2) 2 ⊆ J)
(hV :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 (ρ + 1)) (Set.Ioo (-2) 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (V z) ≤ M)
(y₀ : CKN.Foundation.Parabolic.Vec3)
(hy₀ : y₀ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
(ε : ℝ)
(hε : 0 < ε)
(hseed :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball y₀ ε) (Set.Ioo (-1) 1)), weakVorticity DV z = 0)
:
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (-1) 1)), weakVorticity DV z = 0
On a unit-scale slab of bounded velocity, the weak vorticity of a suitable solution vanishes as soon as it vanishes near one point of the slab.