Ess Local Proof Backward Uniqueness #
Local endpoint regularity through vorticity estimates and backward uniqueness.
theorem
ESS.essLocal_exteriorVorticityZero_halfSpace
(R C : ℝ)
(hR : 0 < R)
(hC : 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)
(hωCont :
ContinuousOn ω
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R < CKN.Foundation.Parabolic.vec3EuclideanNorm x}
(Set.Ioc (-2) 0)))
(hωtop : ∀ (x : CKN.Foundation.Parabolic.Vec3), R < CKN.Foundation.Parabolic.vec3EuclideanNorm x → ω (x, 0) = 0)
(hωbound :
∀ (x : CKN.Foundation.Parabolic.Vec3),
R < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
∀ t ∈ Set.Ioc (-2) 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (ω (x, t)) ≤ C)
(hωderiv :
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | R < CKN.Foundation.Parabolic.vec3EuclideanNorm x}
(Set.Ioo (-2) 0) ω Dω D2ω Dtω)
(hωL2 :
∀
S ⊆
CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R < CKN.Foundation.Parabolic.vec3EuclideanNorm x}
(Set.Ioo (-2) 0),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖ω z‖ₑ ^ 2 + ‖Dω z‖ₑ ^ 2 + ‖D2ω z‖ₑ ^ 2 + ‖Dtω z‖ₑ ^ 2 < ⊤)
(hωineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R < CKN.Foundation.Parabolic.vec3EuclideanNorm x}
(Set.Ioo (-2) 0)), (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)))
(x : CKN.Foundation.Parabolic.Vec3)
:
The terminal vorticity extension vanishes on a fixed exterior half-space throughout its two-unit past slab, by two applications of backward uniqueness.