Space-time pairings for weak vorticity #
Spatial weak integration by parts identifies the distributional curl pairing on a local space-time box.
theorem
ESS.suitableWeakVorticityPairingOnBox
{Ω : 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 * (have this := ψ;
this)
z i = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω' J, ∑ i : Fin 3,
u z i * (have this := vorticityTestCurl ψ;
this)
z i
Pairing weak vorticity against a smooth compact field is the velocity
pairing against its curl on every local box (manuscript
lem:vorticity-weak-eq).