Local integrability and convection pairings for vorticity #
The suitable solution supplies the integrability and spatial pairing needed
for the weak vorticity identity (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakVorticityTestComponentIntegrableOnBox
{Ω : 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 → ℝ}
(hdata : CKN.IsSuitableWeakSolutionData Ω 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)
(i : Fin 3)
:
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => weakVorticity Du z i * φ z i)
(CKN.spaceTimeSet Ω' J) MeasureTheory.volume
Each weak-vorticity component paired with a compact test component is
integrable on a local box (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakVorticityFluxTestIntegrableOnBox
{Ω : 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)
:
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
∑ j : Fin 3,
∑ i : Fin 3,
vorticityFlux u Du z j i * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w i) j z)
(CKN.spaceTimeSet Ω' J) MeasureTheory.volume
The weak-vorticity flux paired with a spatial derivative of a compact
field is integrable on a local box (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakConvectionPairingOnBox
{Ω : 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,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) j z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω' J, ∑ i : Fin 3, spatialCross (u z) (weakVorticity Du z) i * vorticityTestCurl ψ z i
The nonlinear momentum pairing against the curl of a test equals the space-time pairing with velocity crossed with weak vorticity.