Distributional vorticity equation #
The curl of the suitable momentum identity gives the local weak equation for
vorticity (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakVorticityEquationOnBox
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(h : CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0)
{Ω' : Set CKN.Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : CKN.localBox Ω I Ω' J)
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I)
(hψbox :
tsupport
(have this := ψ;
this) ⊆
CKN.spaceTimeSet Ω' J)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω' J, -∑ i : Fin 3,
weakVorticity Du z i * vorticityTestTimeDerivative ψ
(have this := z;
this)
i - ∑ i : Fin 3,
weakVorticity Du z i * vorticityTestLaplacian ψ
(have this := z;
this)
i = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω' J, ∑ j : Fin 3,
∑ i : Fin 3,
vorticityFlux u Du z j i * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w i) j z
The weak vorticity equation holds on any local box containing the support
of the test field (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakVorticityEquation
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
(hIord : I.OrdConnected)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(h : CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0)
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, -∑ i : Fin 3,
weakVorticity Du z i * vorticityTestTimeDerivative ψ
(have this := z;
this)
i - ∑ i : Fin 3,
weakVorticity Du z i * vorticityTestLaplacian ψ
(have this := z;
this)
i = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, ∑ j : Fin 3,
∑ i : Fin 3,
vorticityFlux u Du z j i * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w i) j z
The distributional vorticity identity holds for every compact test on an
open cylinder (manuscript lem:vorticity-weak-eq).