The vorticity regularity theorem #
thm:vorticity-regularity: for a suitable weak solution with zero force whose velocity is
bounded by M on Q₁(x₀, t₀) and whose gradient has energy at most E² there, the vorticity has
on Q_{1/2}(x₀, t₀) a representative which is continuous up to the top time, has space-time
weak derivatives in L², is bounded, and satisfies |∂ₜω - Δω| ≤ C (|ω| + |∇ω|), with C
depending only on M and E.
theorem
ESS.vorticity_restrict_cylinder_half
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ : ℝ)
:
MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (1 / 2)) = MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀)
Restricted to the half cylinder, Lebesgue measure does not see the top time.
theorem
ESS.vorticity_lintegral_sq_lt_top
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
(hf : MeasureTheory.MemLp f 2 μ)
:
The finiteness of the integral of the squared norm of a square-integrable field.
theorem
ESS.vorticity_lintegral_four_lt_top
{α : Type u_1}
{E₁ : Type u_2}
{E₂ : Type u_3}
{E₃ : Type u_4}
{E₄ : Type u_5}
[MeasurableSpace α]
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedAddCommGroup E₃]
[NormedAddCommGroup E₄]
{μ : MeasureTheory.Measure α}
{f₁ : α → E₁}
{f₂ : α → E₂}
{f₃ : α → E₃}
{f₄ : α → E₄}
(h₁ : MeasureTheory.MemLp f₁ 2 μ)
(h₂ : MeasureTheory.MemLp f₂ 2 μ)
(h₃ : MeasureTheory.MemLp f₃ 2 μ)
(h₄ : MeasureTheory.MemLp f₄ 2 μ)
:
The finiteness of the sum of the squared norms of four square-integrable fields.
theorem
ESS.vorticityRegularity
(q M E : ℝ)
:
5 / 2 < q →
0 ≤ M →
0 ≤ E →
∃ (C : ℝ),
0 ≤ C ∧ ∀ (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : 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 → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ),
IsOpen Ω →
IsOpen I →
CKN.IsSuitableWeakSolution Ω I q v Dv pv 0 →
closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1) ⊆ CKN.spaceTimeSet Ω I →
(∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ≤ M) →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1, ‖Dv z‖ₑ ^ 2 ≤ ENNReal.ofReal (E ^ 2) →
∃ (ω : 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),
ω =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (1 / 2))]
weakVorticity Dv ∧ ContinuousOn ω (closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (1 / 2))) ∧ CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2))
(Set.Ioo (t₀ - 1 / 4) t₀) ω Dω D2ω Dtω ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (1 / 2), ‖ω z‖ₑ ^ 2 + ‖Dω z‖ₑ ^ 2 + ‖D2ω z‖ₑ ^ 2 + ‖Dtω z‖ₑ ^ 2 < ⊤ ∧ (∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (1 / 2)), (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))) ∧ ∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (1 / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ω z) ≤ C
thm:vorticity-regularity.