The bound of the velocity gradient #
At every time the smooth approximations of the velocity gradient are bounded pointwise, by the
H² embedding, the div–curl chain and the uniform-in-time bounds of the vorticity and its first
and second derivatives; the bound passes to the weak gradient (the gradient bound
eq:vorticity-regularity-gradient of thm:vorticity-regularity).
theorem
ESS.vorticityFinal_gradBound
(M Kw K1 K2' : ℝ)
(hM : 0 ≤ M)
:
∃ (K : ℝ),
0 ≤ K ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(G Ω1 F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(D2 Ω2 F' : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(F'' : Fin 3 → Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
a + 1 / 32 < t₀ →
t₀ ≤ a + 1 →
(∀ (i : Fin 3),
MeasureTheory.MemLp (U i) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ᵐ (z :
CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀), ∀ (i : Fin 3), |U i z| ≤ M) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (G i j) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j k : Fin 3),
MeasureTheory.MemLp (D2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (Ω1 i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j k : Fin 3),
MeasureTheory.MemLp (Ω2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (F i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j m : Fin 3),
MeasureTheory.MemLp (F' i j m) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j m k : Fin 3),
MeasureTheory.MemLp (F'' i j m k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, G i j y * ψ y) →
(∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, D2 i j k y * ψ y) →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω1 i j y * ψ y) →
(∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω2 i j k y * ψ y) →
(∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, U i y * CKN.spatialPartial ψ i y = 0) →
(∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, vorticityCurl G i y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, F i j y * CKN.spatialPartial ψ j y) →
(∀ (i m : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω1 i m y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, F' i j m y * CKN.spatialPartial ψ j y) →
(∀ (i m k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω2 i m k y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, F'' i j m k y * CKN.spatialPartial ψ j y) →
(∀ (i : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, vorticityCurl G i y ^ 2 + ∑ j : Fin 3, F i j y ^ 2 ≤ Kw) →
(∀ (i m : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω1 i m y ^ 2 + ∑ j : Fin 3, F' i j m y ^ 2 ≤ K1) →
(∀ (i m k : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, Ω2 i m k y ^ 2 + ∑ j : Fin 3, F'' i j m k y ^ 2 ≤ K2') →
∀ᵐ (z :
CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (38 / 64) ×ˢ Set.Ioo (a + 1 / 64) t₀), ∀ (i j : Fin 3), |G i j z| ≤ K
The pointwise bound of the velocity gradient on a smaller box.