The div–curl chain at a fixed time #
At a fixed time, three applications of the div–curl estimate and one of the H² to L∞
embedding bound the smooth approximations of the first, second and third derivatives of the
velocity, and the gradient pointwise, by the vorticity and its derivatives (the velocity levels
of thm:vorticity-regularity).
theorem
ESS.vorticityChain
{ρ : ℝ}
(hρ : 4 / 64 < ρ)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (U w : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(D2 Ω2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (i : Fin 3), ContDiff ℝ (↑⊤) (U i)) →
(∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (G i j)) →
(∀ (i j k : Fin 3), ContDiff ℝ (↑⊤) (D2 i j k)) →
(∀ (i : Fin 3), Continuous (w i)) →
(∀ (i j : Fin 3), Continuous (Ω1 i j)) →
(∀ (i j k : Fin 3), Continuous (Ω2 i j k)) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ, ∑ i : Fin 3, CKN.spatialPartial (U i) i (x, t) = 0) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (i k : Fin 3),
CKN.spatialPartial (U k) i (x, t) - CKN.spatialPartial (U i) k (x, t) = vorticityAntisym (fun (l : Fin 3) => w l (x, t)) i k) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (i j : Fin 3), CKN.spatialPartial (U i) j (x, t) = G i j (x, t)) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (m : Fin 3), ∑ i : Fin 3, CKN.spatialPartial (G i m) i (x, t) = 0) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (m i k : Fin 3),
CKN.spatialPartial (G k m) i (x, t) - CKN.spatialPartial (G i m) k (x, t) = vorticityAntisym (fun (l : Fin 3) => Ω1 l m (x, t)) i k) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (i j k : Fin 3), CKN.spatialPartial (G i j) k (x, t) = D2 i j k (x, t)) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (j k : Fin 3), ∑ i : Fin 3, CKN.spatialPartial (D2 i j k) i (x, t) = 0) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ ρ,
∀ (j k i c : Fin 3),
CKN.spatialPartial (D2 c j k) i (x, t) - CKN.spatialPartial (D2 i j k) c (x, t) = vorticityAntisym (fun (l : Fin 3) => Ω2 l j k (x, t)) i c) →
∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (ρ - 1 / 64), ∑ i : Fin 3, ∑ j : Fin 3, G i j (x, t) ^ 2 ≤ C * ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ ρ, ∑ l : Fin 3, w l (x, t) ^ 2 + ∑ i : Fin 3, U i (x, t) ^ 2 ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (ρ - 2 / 64), ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2 i j k (x, t) ^ 2 ≤ C * ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (ρ - 1 / 64), ∑ l : Fin 3, ∑ m : Fin 3, Ω1 l m (x, t) ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, G i j (x, t) ^ 2 ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (ρ - 3 / 64), ∑ i : Fin 3,
∑ j : Fin 3,
∑ k : Fin 3, ∑ c : Fin 3, CKN.spatialPartial (D2 i j k) c (x, t) ^ 2 ≤ C * ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (ρ - 2 / 64), ∑ l : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, Ω2 l j k (x, t) ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2 i j k (x, t) ^ 2 ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3),
CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ ρ - 4 / 64 →
∀ (i j : Fin 3),
G i j (x, t) ^ 2 ≤ C * ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (ρ - 3 / 64), G i j (y, t) ^ 2 + ∑ k : Fin 3, D2 i j k (y, t) ^ 2 + ∑ k : Fin 3,
∑ c : Fin 3, CKN.spatialPartial (D2 i j k) c (y, t) ^ 2
The div–curl chain at a fixed time, on the balls of radii ρ, ρ - 1/64, …, ρ - 4/64.