Vorticity vanishing near a regular time #
Near a time t₀ at which a whole closed ball times a time interval consists of
regular points (lem:time-projection), the velocity is bounded on a compact
slab. A parabolic rescaling turns that slab into the unit-scale slab of
essLocal_slabVorticityZero, and the vanishing of the weak vorticity on an
exterior half-space seeds the continuation argument in the proof of
thm:ess-local (time-slice and spatial unique continuation).
theorem
ESS.essLocal_weakVorticity_parabolicRescale
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r : ℝ)
(DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
weakVorticity (parabolicRescaleGradient x₀ t₀ r DU) z = r ^ 2 • weakVorticity DU (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))
The weak vorticity of the rescaled gradient is the rescaled weak vorticity.
theorem
ESS.essLocal_regularSlab_vorticityZero
{U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hsws : CKN.IsSuitableWeakSolution Set.univ (Set.Ioo (-12) 0) 3 U DU q 0)
(R₂ ρ : ℝ)
(hR₂ : 0 < R₂)
(hρ : R₂ < ρ)
(hseed :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R₂ < x 2} (Set.Ioo (-2) 0)), weakVorticity DU z = 0)
(t₀ : ℝ)
(ht₀ : t₀ ∈ Set.Ioo (-2) 0)
(hreg :
∀ (ρ' : ℝ),
0 < ρ' →
∃ δ > 0,
closure (CKN.Foundation.Parabolic.vec3Ball 0 ρ') ×ˢ Set.Ioo (t₀ - δ) (t₀ + δ) ⊆
regularPointLocus (Set.Ioo (-12) 0) U)
:
∃ (ε : ℝ),
0 < ε ∧ ∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (t₀ - ε) (t₀ + ε))), weakVorticity DU z = 0
Near a time at which closed balls times short intervals consist of regular
points, the weak vorticity of a global suitable solution vanishes on any ball
of radius larger than R₂, provided it vanishes on the half-space
{x₃ > R₂} throughout (-2, 0).