Weak vorticity equation

The slice weak-gradient data in suitability identify the explicit velocity gradient used to define vorticity.

noncomputable def ESS.spatialTestCurl (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The spatial curl of a smooth vector test field.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ESS.spatialTestCurl_zero (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : spatialTestCurl ψ x 0 = CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y 2) 1 x - CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y 1) 2 x

@[simp]

theorem ESS.spatialTestCurl_one (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : spatialTestCurl ψ x 1 = CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y 0) 2 x - CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y 2) 0 x

@[simp]

theorem ESS.spatialTestCurl_two (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : spatialTestCurl ψ x 2 = CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y 1) 0 x - CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y 0) 1 x

def ESS.spatialCross (u ω : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The classical cross product in the native three-component carrier.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ESS.spatialCross_zero (u ω : CKN.Foundation.Parabolic.Vec3) : spatialCross u ω 0 = u 1 * ω 2 - u 2 * ω 1

@[simp]

theorem ESS.spatialCross_one (u ω : CKN.Foundation.Parabolic.Vec3) : spatialCross u ω 1 = u 2 * ω 0 - u 0 * ω 2

@[simp]

theorem ESS.spatialCross_two (u ω : CKN.Foundation.Parabolic.Vec3) : spatialCross u ω 2 = u 0 * ω 1 - u 1 * ω 0

def ESS.spatialWeakVorticity (Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The curl determined by a spatial weak gradient.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ESS.spatialWeakVorticity_zero (Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : spatialWeakVorticity Du x 0 = Du x 2 1 - Du x 1 2

@[simp]

theorem ESS.spatialWeakVorticity_one (Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : spatialWeakVorticity Du x 1 = Du x 0 2 - Du x 2 0

@[simp]

theorem ESS.spatialWeakVorticity_two (Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : spatialWeakVorticity Du x 2 = Du x 1 0 - Du x 0 1

theorem ESS.spatialConvective_decomposition (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : ∑ j : Fin 3, u x j * Du x i j = ∑ j : Fin 3, u x j * Du x j i - spatialCross (u x) (spatialWeakVorticity Du x) i

The weak-gradient curl gives the usual convective-term identity in three dimensions.

theorem ESS.suitableWeakConvectionProductPairing {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hUfinite : (MeasureTheory.volume.restrict U) Set.univ < ⊤) {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 2 (MeasureTheory.volume.restrict U)) (hDv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Dv x i) 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), CKN.HasWeakGradientOn U (fun (x : CKN.Vec 3) => v x i) fun (x : CKN.Vec 3) => Dv x i) {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφU : tsupport φ ⊆ U) (i : Fin 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, ∑ j : Fin 3, v x i * v x j * CKN.spatialDeriv φ j x = -∫ (x : CKN.Foundation.Parabolic.Vec3) in U, ∑ j : Fin 3, (Dv x i j * v x j + v x i * Dv x j j) * φ x

A spatial product pairing for the convection tensor, obtained from the slice weak-gradient identities (manuscript lem:vorticity-weak-eq).

theorem ESS.suitableWeakConvectionTensorPairing {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hUfinite : (MeasureTheory.volume.restrict U) Set.univ < ⊤) {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 2 (MeasureTheory.volume.restrict U)) (hDv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Dv x i) 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), CKN.HasWeakGradientOn U (fun (x : CKN.Vec 3) => v x i) fun (x : CKN.Vec 3) => Dv x i) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφ : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) (hφc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) (hφU : ∀ (i : Fin 3), (tsupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) ⊆ U) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, ∑ j : Fin 3, v x i * v x j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => φ y i) j x = -∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, ∑ j : Fin 3, (Dv x i j * v x j + v x i * Dv x j j) * φ x i

The vector convection tensor paired against a compact smooth field reduces to the weak-gradient product rule on suitable slices (manuscript lem:vorticity-weak-eq).

theorem ESS.suitableWeakGradientPairingZero {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hUfinite : (MeasureTheory.volume.restrict U) Set.univ < ⊤) {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 2 (MeasureTheory.volume.restrict U)) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), CKN.HasWeakGradientOn U (fun (x : CKN.Vec 3) => v x i) fun (x : CKN.Vec 3) => Dv x i) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφ : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) (hφc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) (hφU : ∀ (i : Fin 3), (tsupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) ⊆ U) (hdivφ : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => φ y i) i x = 0) : ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, v x j * Dv x j i * φ x i = 0

The gradient part of convection pairs to zero against a divergence-free compact test field (manuscript lem:vorticity-weak-eq).

theorem ESS.vorticityFlux_spatialTestCurl_pairing (u ω : CKN.Foundation.Parabolic.Vec3) (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) : ∑ j : Fin 3, ∑ i : Fin 3, (u j * ω i - ω j * u i) * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j x = ∑ k : Fin 3, spatialCross u ω k * spatialTestCurl ψ x k

The antisymmetric flux pairing is the cross-product pairing with the spatial curl of the test field.

noncomputable def ESS.vorticityTestPartial (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The CKN spatial partial derivative written on ordinary product coordinates.

Equations

• ESS.vorticityTestPartial f i z = (fderiv ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, z.2)) z.1) (CKN.basisVec i)

theorem ESS.vorticityTestPartial_eq_spatialPartial (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestPartial f i z = CKN.spatialPartial f i z

noncomputable def ESS.vorticityTestCurl (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.Foundation.Parabolic.Vec3

The classical spatial curl of a smooth vector test field, using CKN's factor-wise spatial partial derivatives (manuscript lem:vorticity-weak-eq).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ESS.vorticityTestCurl_zero (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestCurl ψ z 0 = vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w 2) 1 z - vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w 1) 2 z

@[simp]

theorem ESS.vorticityTestCurl_one (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestCurl ψ z 1 = vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w 0) 2 z - vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w 2) 0 z

@[simp]

theorem ESS.vorticityTestCurl_two (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestCurl ψ z 2 = vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w 1) 0 z - vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w 0) 1 z

theorem ESS.vorticityTestCurl_mem_spaceTimeTestFunction {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I) : vorticityTestCurl ψ ∈ CKN.spaceTimeTestFunction Ω I

Curl preserves the compact smooth test class and its support.

theorem ESS.vorticityTestPartial_spatialPartial_commute {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestPartial ψ i w) j z = vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestPartial ψ j w) i z

Mixed spatial derivatives of a smooth scalar test commute, expressed in product coordinates (manuscript lem:vorticity-weak-eq).

theorem ESS.vorticityTestPartial_sub_smooth {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => f w - g w) i z = vorticityTestPartial f i z - vorticityTestPartial g i z

Spatial differentiation distributes over subtraction of smooth tests.

theorem ESS.vorticityTestCurl_divergence {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ∑ i : Fin 3, vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) i z = 0

The curl test is divergence-free.

theorem ESS.suitableWeakGradientOnSlices {Ω : 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) (i : Fin 3) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, CKN.HasWeakGradientOn Ω' (fun (x : CKN.Vec 3) => u (x, s) i) fun (x : CKN.Vec 3) => Du (x, s) i

Suitable solutions carry the spatial weak-gradient identity on almost every time slice of each local box (manuscript lem:vorticity-weak-eq).

theorem ESS.suitableWeakGradientTraceZeroOnBox {Ω : 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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, Du (x, s) i i) =ᵐ[MeasureTheory.volume.restrict Ω'] 0

The spatial weak-gradient trace vanishes on almost every local slice of a suitable solution (manuscript lem:vorticity-weak-eq).

theorem ESS.suitableWeakSpatialIntegrationByParts {Ω : 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 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψsupport : tsupport ψ ⊆ Ω' ×ˢ J) (i j : Fin 3) : ∫ (t : ℝ) in J, ∫ (x : CKN.Foundation.Parabolic.Vec3) in Ω', Du (x, t) i j * ψ (x, t) = -∫ (t : ℝ) in J, ∫ (x : CKN.Foundation.Parabolic.Vec3) in Ω', u (x, t) i * CKN.spatialPartial ψ j (x, t)

Slice weak gradients integrate by parts against smooth space-time tests on a local box (manuscript lem:vorticity-weak-eq).