Smooth spatial energy inequality for vorticity #
The component balance is combined with finite-dimensional estimates to
obtain the spatial differential inequality used in lem:localized-vorticity-energy.
theorem
ESS.smoothVorticityEnergyDifferentialInequality
{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}
(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)
(hzc : ∀ (t : ℝ), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, t))
(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)
(M : ℝ)
(hM : 0 ≤ M)
(hvbound : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (v (x, t)) ≤ M)
(hF2 :
∀ (t : ℝ),
MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, ∑ i : Fin 3, F (x, t) j i ^ 2)
MeasureTheory.volume)
(hg2 :
∀ (t : ℝ),
MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, g (x, t) i ^ 2)
MeasureTheory.volume)
(t : ℝ)
:
(2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) (x, t) * z (x, t) i) + ∫ (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 ≤ (((72 * M ^ 2 + 1) * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, z (x, t) i ^ 2) + 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
A smooth compactly supported solution of the linear vorticity equation
satisfies the spatial differential energy inequality used in the smooth part
of lem:localized-vorticity-energy. Both matrix and vector forcing are measured in L² in this
smooth estimate.
theorem
ESS.smoothVorticityEnergyDifferentialInequality_commonSupport
{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}
(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)
(M : ℝ)
(hM : 0 ≤ M)
(hvbound : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (v (x, t)) ≤ M)
(t : ℝ)
:
(2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) (x, t) * z (x, t) i) + ∫ (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 ≤ (((72 * M ^ 2 + 1) * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, z (x, t) i ^ 2) + 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
The smooth spatial energy inequality applies to fields with one common
compact spatial support, the support condition used in smooth approximation
for lem:localized-vorticity-energy.