Convolution calculus for the local energy inequality

Convolutions of square-integrable fields with a smooth compactly supported kernel are smooth, their partial derivatives are the convolutions with the partial derivatives of the kernel, integration by parts moves these derivatives onto a smooth compactly supported factor, and the convolution of a weakly divergence-free field with the kernel gradient has zero trace. These are the spatial computations of eq:reg-local-energy-forced.

noncomputable def CKN.Leray.leConv (κ g : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.Vec3 → ℝ

The scalar convolution κ ⋆ g.

Equations

• CKN.Leray.leConv κ g = MeasureTheory.convolution κ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

theorem CKN.Leray.leConv_contDiff {κ : Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) : ContDiff ℝ (↑⊤) (leConv κ g)

theorem CKN.Leray.fderiv_leConv {κ : Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (j : Fin 3) : (fderiv ℝ (leConv κ g) x) (basisVec j) = leConv (spatialDeriv κ j) g x

theorem CKN.Leray.integral_mul_reflect_eq_leConv (g κ' : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) : ∫ (y : Foundation.Parabolic.Vec3), g y * κ' (x - y) = leConv κ' g x

theorem CKN.Leray.integral_mul_leConv_spatialDeriv {κ : Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) {a : Foundation.Parabolic.Vec3 → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hac : HasCompactSupport a) (j : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), a x * leConv (spatialDeriv κ j) g x = -∫ (x : Foundation.Parabolic.Vec3), (fderiv ℝ a x) (basisVec j) * leConv κ g x

Integration by parts of a kernel derivative against a smooth compactly supported factor.

theorem CKN.Leray.sum_leConv_spatialDeriv_eq_zero {κ : Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hu : IsWeakDivFreeL2 u) (x : Foundation.Parabolic.Vec3) : ∑ k : Fin 3, leConv (spatialDeriv κ k) (fun (y : Foundation.Parabolic.Vec3) => u y k) x = 0

The convolution of a weakly divergence-free field with the kernel gradient has zero trace.