Ess Local Proof Interior Vorticity

Local endpoint regularity through vorticity estimates and backward uniqueness.

theorem ESS.essLocal_regularPoint_velocityBound {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {z₀ : CKN.Foundation.Parabolic.ParabolicPoint} (hreg : CKN.IsRegularPoint Ω I u z₀) : ∃ (N : Set CKN.Foundation.Parabolic.ParabolicPoint), IsOpen N ∧ z₀ ∈ N ∧ N ⊆ CKN.spaceTimeSet Ω I ∧ ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict N, CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ M

A CKN regular point has a neighborhood on which the velocity is essentially bounded.

theorem ESS.essLocal_regularTimes_localVelocityBound {I : Set ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hregular : ∀ᵐ (t : ℝ), t ∈ I → ∀ (ρ : ℝ), 0 < ρ → ∃ δ > 0, closure (CKN.Foundation.Parabolic.vec3Ball 0 ρ) ×ˢ Set.Ioo (t - δ) (t + δ) ⊆ regularPointLocus I u) : ∀ᵐ (t : ℝ), t ∈ I → ∀ (x : CKN.Foundation.Parabolic.Vec3), ∃ (N : Set CKN.Foundation.Parabolic.ParabolicPoint), IsOpen N ∧ (x, t) ∈ N ∧ N ⊆ CKN.spaceTimeSet Set.univ I ∧ ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict N, CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ M

At almost every time supplied by the projection theorem, every spatial point has a neighborhood with an essential velocity bound.

theorem ESS.essLocal_regularCompact_velocityBound {I : Set ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) (hKreg : K ⊆ regularPointLocus I u) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict K, CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ M

A compact subset of the regular-point locus has one essential velocity bound.