Estimates at a fixed time for smooth approximations #
The div–curl estimate and the H² to L∞ embedding applied to the time slices of smooth
space-time fields whose divergence, antisymmetric derivatives or first derivatives are prescribed
on a ball (lem:local-div-curl and the embedding step of thm:vorticity-regularity), and the
locality of backward mollification.
theorem
ESS.vorticity_divCurl_slice
{r R : ℝ}
(hr : 0 < r)
(hrR : r < R)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (V Φ : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (b : Fin 3), ContDiff ℝ (↑⊤) (V b)) →
(∀ (l : Fin 3), Continuous (Φ l)) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R, ∑ a : Fin 3, CKN.spatialPartial (V a) a (x, t) = 0) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R,
∀ (a b : Fin 3),
CKN.spatialPartial (V b) a (x, t) - CKN.spatialPartial (V a) b (x, t) = vorticityAntisym (fun (l : Fin 3) => Φ l (x, t)) a b) →
∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ r, ∑ a : Fin 3, ∑ b : Fin 3, CKN.spatialPartial (V b) a (x, t) ^ 2 ≤ C * ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ R, ∑ l : Fin 3, Φ l (x, t) ^ 2 + ∑ b : Fin 3, V b (x, t) ^ 2
The div–curl estimate on a time slice.
theorem
ESS.vorticity_sobolev_slice
{r R : ℝ}
(hr : 0 < r)
(hrR : r < R)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(g : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) f →
(∀ (j : Fin 3), ContDiff ℝ (↑⊤) (g j)) →
(∀ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R, ∀ (j : Fin 3), CKN.spatialPartial f j (x, t) = g j (x, t)) →
∀ (x : CKN.Foundation.Parabolic.Vec3),
CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ r →
f (x, t) ^ 2 ≤ C * ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ R, f (y, t) ^ 2 + ∑ j : Fin 3, g j (y, t) ^ 2 + ∑ j : Fin 3, ∑ k : Fin 3, CKN.spatialPartial (g j) k (y, t) ^ 2
The H² to L∞ embedding on a time slice, for a smooth field with prescribed first
derivatives on a ball.
theorem
ESS.vorticityBackMollify_antisym
{W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)}
(hW : MeasurableSet W)
{v : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hv : ∀ (l : Fin 3), MeasureTheory.IntegrableOn (v l) W MeasureTheory.volume)
{ε : ℝ}
(hε : 0 < ε)
(i k : Fin 3)
(z : CKN.Foundation.Parabolic.Vec3 × ℝ)
:
CKN.vorticityBackMollify W
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityAntisym (fun (l : Fin 3) => v l y) i k) ε hε z = vorticityAntisym (fun (l : Fin 3) => CKN.vorticityBackMollify W (v l) ε hε z) i k
Backward mollification commutes with the antisymmetric matrix of a vector field.