Space-time weak vorticity equation #
Compact tests are localized to CKN local boxes, where the suitable solution provides almost-everywhere spatial weak gradients.
theorem
ESS.integralOn_eq_of_subset_of_zero_off
{S K : Set CKN.Foundation.Parabolic.ParabolicPoint}
{f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hKS : K ⊆ S)
(hf : ∀ z ∉ K, f z = 0)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, f z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, f z
A compactly supported integrand has the same integral over any set that
contains its support and over its support (manuscript
lem:vorticity-weak-eq).
theorem
ESS.vorticitySpatialPartialTest
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Ω I)
(j : Fin 3)
:
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial φ j z) ∈ CKN.spaceTimeTestFunction Ω I
A CKN scalar test remains a test after taking a spatial derivative.
theorem
ESS.vorticityTimePartialTest
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Ω I)
:
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial φ z) ∈ CKN.spaceTimeTestFunction Ω I
A CKN scalar test remains a test after time differentiation.
theorem
ESS.localBox_spaceTimeSet_nullMeasurable
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{Ω' : Set CKN.Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : CKN.localBox Ω I Ω' J)
:
The space-time set of a CKN local box is null-measurable for the
parabolic volume measure (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakVelocityTestIntegrableOnBox
{Ω : 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 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Ω I)
(i : Fin 3)
:
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z i * φ z) (CKN.spaceTimeSet Ω' J)
MeasureTheory.volume
Suitable velocity components multiplied by a compact test are integrable
on every local box (manuscript lem:vorticity-weak-eq).
theorem
ESS.suitableWeakGradientTestIntegrableOnBox
{Ω : 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 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Ω I)
(i j : Fin 3)
:
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Du z i j * φ z) (CKN.spaceTimeSet Ω' J)
MeasureTheory.volume
Suitable weak-gradient components multiplied by a compact test are
integrable on every local box (manuscript lem:vorticity-weak-eq).
theorem
ESS.vorticity_integral_on_box_eq_iterated
{Ω' : Set CKN.Foundation.Parabolic.Vec3}
{J : Set ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : MeasureTheory.IntegrableOn f (CKN.spaceTimeSet Ω' J) MeasureTheory.volume)
:
Fubini's theorem in the native parabolic carrier identifies a local space-time integral with its time-first iterated integral.
theorem
ESS.suitableWeakMomentumTestCurl
{Ω : 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)
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, -∑ i : Fin 3, u z i * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) z - ∑ 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 + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) j z = 0
Testing the suitable momentum equation with the curl of a compact test
field removes the pressure and zero force terms (manuscript
lem:vorticity-weak-eq).
theorem
ESS.suitableWeakMomentumTestCurlOnSupport
{Ω : 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)
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in tsupport
(have this := vorticityTestCurl ψ;
this), -∑ i : Fin 3, u z i * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) z - ∑ 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 + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) j z = 0
The curl-tested momentum identity can be restricted to the compact support
of the test curl (manuscript lem:vorticity-weak-eq).