Smooth spatial energy identity for vorticity

The compactly supported smooth energy calculation is the first step in lem:localized-vorticity-energy.

theorem ESS.vorticityEnergy_component_hasCompactSupport {z : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {t : ℝ} (hz : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, t)) (i : Fin 3) : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, t) i

A component of a compactly supported spatial slice remains compactly supported (manuscript lem:localized-vorticity-energy).

theorem ESS.vorticityEnergy_integrable_mul_compact {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : Continuous f) (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) MeasureTheory.volume

A smooth factor times a compactly supported smooth factor is integrable (manuscript lem:localized-vorticity-energy).

theorem ESS.vorticityEnergy_slice_contDiff {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)

Restricting a smooth space-time scalar field to a time slice preserves smoothness (manuscript lem:localized-vorticity-energy).

theorem ESS.vorticityEnergy_first_slice_hasCompactSupport {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {t : ℝ} (hfc : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) (j : Fin 3) : HasCompactSupport (CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) j)

Every first spatial derivative of a compactly supported smooth slice has compact support (manuscript lem:localized-vorticity-energy).

theorem ESS.vorticityEnergy_fieldComponent_contDiff {z : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hz : ContDiff ℝ (↑⊤) z) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i

A component of a smooth vector-valued space-time field is smooth (manuscript lem:localized-vorticity-energy).

theorem ESS.vorticityEnergy_integral_finsetSum {f : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ∀ (i : Fin 3), MeasureTheory.Integrable (f i) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f i x = ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), f i x

Integrals commute with finite sums of integrable vorticity components (manuscript lem:localized-vorticity-energy).

theorem ESS.vorticityEnergy_integral_finsetSum2 {f : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ∀ (i j : Fin 3), MeasureTheory.Integrable (f i j) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, f i j x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), f i j x

Iterated finite sums commute with integration for integrable terms (manuscript lem:localized-vorticity-energy).

theorem ESS.smoothVorticityComponentEnergyBalance {v z : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {F : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ} {g : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hv : ContDiff ℝ (↑⊤) v) (hz : ContDiff ℝ (↑⊤) z) (hF : ∀ (j i : Fin 3), ContDiff ℝ ↑⊤ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => F w j i) (hg : ContDiff ℝ (↑⊤) g) (hzc : ∀ (t : ℝ), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, t)) (heq : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (i : Fin 3), CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) (x, t) - ∑ j : Fin 3, CKN.spatialSecondPartial (have this := fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => z w i; this) j j (x, t) = -∑ j : Fin 3, CKN.spatialPartial (have this := fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => v w j * z w i - z w j * v w i; this) j (x, t) + ∑ j : Fin 3, CKN.spatialPartial (have this := fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => F w j i; this) j (x, t) + g (x, t) i) (t : ℝ) (i : Fin 3) : (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) (x, t) * z (x, t) i) + ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) j (x, t) ^ 2 = ((∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), (v (x, t) j * z (x, t) i - z (x, t) j * v (x, t) i) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) j (x, t)) - ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F (x, t) j i * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => z w i) j (x, t)) + ∫ (x : CKN.Foundation.Parabolic.Vec3), g (x, t) i * z (x, t) i

A smooth solution of a linear vorticity equation satisfies its spatial energy balance when paired with one component of the solution itself (manuscript lem:localized-vorticity-energy).