Time-integrated smooth vorticity energy #
Compact spatial support lets the spatial differential estimate pass through the time integral and the scalar Grönwall bound.
theorem
ESS.smoothVorticityEnergyGronwall
{a b M e₀ : ℝ}
{v z : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ}
{g : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hab : a ≤ b)
(hM : 0 ≤ M)
(hv : ContDiff ℝ (↑⊤) v)
(hz : ContDiff ℝ (↑⊤) z)
(hF : ∀ (j i : Fin 3), ContDiff ℝ ↑⊤ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => F w j i)
(hg : ContDiff ℝ (↑⊤) g)
(hcommon :
∃ (K : Set CKN.Foundation.Parabolic.Vec3),
IsCompact K ∧ ∀ x ∉ K, ∀ (t : ℝ), z (x, t) = 0 ∧ (∀ (j i : Fin 3), F (x, t) j i = 0) ∧ g (x, t) = 0)
(heq :
∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (i : Fin 3),
CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) (x, t) - ∑ j : Fin 3,
CKN.spatialSecondPartial
(have this := fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => z w i;
this)
j j (x, t) = -∑ j : Fin 3,
CKN.spatialPartial
(have this := fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => v w j * z w i - z w j * v w i;
this)
j (x, t) + ∑ j : Fin 3,
CKN.spatialPartial
(have this := fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => F w j i;
this)
j (x, t) + g (x, t) i)
(hvbound : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (v (x, t)) ≤ M)
(hinit : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, z (x, a) i ^ 2 ≤ e₀)
:
have e := fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, z (x, t) i ^ 2;
have d := fun (t : ℝ) =>
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) j (x, t) ^ 2;
have f := fun (t : ℝ) =>
(2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ i : Fin 3, F (x, t) j i ^ 2) + ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, g (x, t) i ^ 2;
(∀ t ∈ Set.Icc a b, e t ≤ Real.exp ((72 * M ^ 2 + 1) * (b - a)) * (e₀ + ∫ (s : ℝ) in a..b, f s)) ∧ ∫ (t : ℝ) in a..b, d t ≤ e₀ + (72 * M ^ 2 + 1) * (b - a) * (Real.exp ((72 * M ^ 2 + 1) * (b - a)) * (e₀ + ∫ (s : ℝ) in a..b, f s)) + ∫ (s : ℝ) in a..b, f s
A smooth, compactly supported solution of the linear vorticity equation
satisfies the time-integrated energy bound obtained from its spatial energy
inequality (manuscript lem:localized-vorticity-energy).