Static identities for the local energy inequality

For a square-integrable weakly differentiable velocity slice u with gradient D and a smooth compactly supported weight ψ, the chain rule ∑ⱼ ∫ D_kj u_k ∂ⱼψ = -½ ∫ u_k² Δψ, the transport identity ∑ⱼ ∫ Vⱼ u_k D_kj ψ = -½ ∫ u_k² V·∇ψ for a divergence-free C¹ field V, and the pressure identity ∑ₖ ∫ u_k ψ Gₖ = -∫ p u·∇ψ for a pressure p with weak gradient G hold, by mollification. These are the spatial identities of eq:reg-local-energy-forced.

theorem CKN.Leray.integral_sq_mul_fderiv {w g : Foundation.Parabolic.Vec3 → ℝ} (hw : ContDiff ℝ (↑⊤) w) (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (j : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), w x ^ 2 * (fderiv ℝ g x) (basisVec j) = -∫ (x : Foundation.Parabolic.Vec3), 2 * (w x * (fderiv ℝ w x) (basisVec j)) * g x

Integration by parts of the square of a smooth function against a smooth compactly supported factor.

theorem CKN.Leray.leConv_leMol_contDiff {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (n : ℕ) : ContDiff ℝ (↑⊤) (leConv (leMol n) g)

theorem CKN.Leray.tendsto_mul_leConv_leMol {g h : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hh : Continuous h) (hhc : HasCompactSupport h) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((fun (x : Foundation.Parabolic.Vec3) => leConv (leMol n) g x * h x) - fun (x : Foundation.Parabolic.Vec3) => g x * h x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

theorem CKN.Leray.memLp_mul_compact {g h : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hh : Continuous h) (hhc : HasCompactSupport h) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => g x * h x) 2 MeasureTheory.volume

theorem CKN.Leray.sum_integral_grad_mul_eq {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hu : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x k) 2 MeasureTheory.volume) {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) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (k : Fin 3) : ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), D x k j * (u x k * (fderiv ℝ ψ x) (basisVec j)) = -(1 / 2) * ∫ (x : Foundation.Parabolic.Vec3), u x k * (u x k * spatialLaplacian ψ x)

The chain rule ∑ⱼ ∫ D_kj u_k ∂ⱼψ = -½ ∫ u_k² Δψ.

theorem CKN.Leray.sum_integral_transport_eq {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hu : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x k) 2 MeasureTheory.volume) {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) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (k : Fin 3) : ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), D x k j * (u x k * (V x j * ψ x)) = -(1 / 2) * ∫ (x : Foundation.Parabolic.Vec3), u x k * (u x k * ∑ j : Fin 3, V x j * (fderiv ℝ ψ x) (basisVec j))

The transport identity ∑ⱼ ∫ D_kj u_k Vⱼ ψ = -½ ∫ u_k² V·∇ψ for a divergence-free C¹ field V.