The limiting energy pairing on one time slice

For a weakly divergence-free square-integrable velocity slice u with weak gradient D, a divergence-free C¹ transport field V, a square-integrable pressure q, a force pressure p_f with square-integrable weak gradient G, a square-integrable force F and a smooth compactly supported weight ψ, the sum over the components of the limiting energy pairings is ∫ |D|² ψ - ½ ∫ (|u|² Δψ + (|u|² V + 2 (q + p_f) u)·∇ψ + 2 (F·u) ψ). This is the spatial identity behind eq:reg-local-energy-forced.

theorem CKN.Leray.integrable_mul_mul_compact {a b c : Foundation.Parabolic.Vec3 → ℝ} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (hb : MeasureTheory.MemLp b 2 MeasureTheory.volume) (hc : Continuous c) (hcc : HasCompactSupport c) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => a x * (b x * c x)) MeasureTheory.volume

A product of two square-integrable functions and a continuous compactly supported weight is integrable.

theorem CKN.Leray.hasCompactSupport_sum_fin_three {g : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (j : Fin 3), HasCompactSupport (g j)) : HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, g j x

theorem CKN.Leray.leLimit_slice_eq {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hdf : IsWeakDivFreeL2 u) {D : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} (hD : ∀ (k j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => D x k j) 2 MeasureTheory.volume) (hweak : ∀ (k : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u x k) fun (x : Vec 3) => D x k) {V : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hV : ∀ (j : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => V x j) (hdiv : ∀ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => V y j) x) (basisVec j) = 0) {q : Foundation.Parabolic.Vec3 → ℝ} (hq : MeasureTheory.MemLp q 2 MeasureTheory.volume) {G F : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (k : Fin 3) : leLimit (fun (x : Foundation.Parabolic.Vec3) => u x k) (fun (j : Fin 3) (x : Foundation.Parabolic.Vec3) => D x k j) (fun (j : Fin 3) (x : Foundation.Parabolic.Vec3) => V x j * u x k - D x k j) q (fun (x : Foundation.Parabolic.Vec3) => G x k) (fun (x : Foundation.Parabolic.Vec3) => F x k) ψ k = ((((((∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), D x k j * (D x k j * ψ x)) - 1 / 2 * ∫ (x : Foundation.Parabolic.Vec3), u x k * (u x k * spatialLaplacian ψ x)) - 1 / 2 * ∫ (x : Foundation.Parabolic.Vec3), u x k * (u x k * ∑ j : Fin 3, V x j * (fderiv ℝ ψ x) (basisVec j))) - ∫ (x : Foundation.Parabolic.Vec3), q x * (D x k k * ψ x)) - ∫ (x : Foundation.Parabolic.Vec3), q x * (u x k * (fderiv ℝ ψ x) (basisVec k))) + ∫ (x : Foundation.Parabolic.Vec3), u x k * (ψ x * G x k)) - ∫ (x : Foundation.Parabolic.Vec3), F x k * (u x k * ψ x)

The limiting energy pairing of one component, after the chain rule and the transport identity.

theorem CKN.Leray.sum_leLimit_slice_eq {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hdf : IsWeakDivFreeL2 u) {D : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} (hD : ∀ (k j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => D x k j) 2 MeasureTheory.volume) (hweak : ∀ (k : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u x k) fun (x : Vec 3) => D x k) {V : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hV : ∀ (j : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => V x j) (hdiv : ∀ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => V y j) x) (basisVec j) = 0) {q : Foundation.Parabolic.Vec3 → ℝ} (hq : MeasureTheory.MemLp q 2 MeasureTheory.volume) {pf : Foundation.Parabolic.Vec3 → ℝ} (hpl : MeasureTheory.LocallyIntegrable pf MeasureTheory.volume) {G : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hG : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => G x k) 2 MeasureTheory.volume) (hpG : HasWeakGradientOn Set.univ pf G) {F : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hF : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F x k) 2 MeasureTheory.volume) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hpψ : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pf x * (fderiv ℝ ψ x) (basisVec k)) 2 MeasureTheory.volume) : ∑ k : Fin 3, leLimit (fun (x : Foundation.Parabolic.Vec3) => u x k) (fun (j : Fin 3) (x : Foundation.Parabolic.Vec3) => D x k j) (fun (j : Fin 3) (x : Foundation.Parabolic.Vec3) => V x j * u x k - D x k j) q (fun (x : Foundation.Parabolic.Vec3) => G x k) (fun (x : Foundation.Parabolic.Vec3) => F x k) ψ k = (∫ (x : Foundation.Parabolic.Vec3), (∑ k : Fin 3, ∑ j : Fin 3, D x k j ^ 2) * ψ x) - 1 / 2 * ∫ (x : Foundation.Parabolic.Vec3), (∑ k : Fin 3, u x k ^ 2) * spatialLaplacian ψ x + ∑ i : Fin 3, ((∑ k : Fin 3, u x k ^ 2) * V x i + 2 * (q x + pf x) * u x i) * (fderiv ℝ ψ x) (basisVec i) + (2 * ∑ i : Fin 3, F x i * u x i) * ψ x

The sum over the components of the limiting energy pairings on one time slice.