Spatial convolution with smooth compact kernels

For a smooth compactly supported kernel k on ℝ³ and a spatial field h, the convolution k ⋆ h is smooth, its partial derivatives are the convolutions with the partial derivatives of k, it is bounded in L² by ‖k‖₁ ‖h‖₂, and it satisfies the whole-space integration by parts identity. These are the spatial tools of the energy argument in lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript.

noncomputable def CKN.vlConv (k h : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.Vec3 → ℝ

Convolution of a spatial field h with a kernel k.

Equations

• CKN.vlConv k h = MeasureTheory.convolution k h (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

noncomputable def CKN.vlDeriv (k : Foundation.Parabolic.Vec3 → ℝ) (j : Fin 3) : Foundation.Parabolic.Vec3 → ℝ

The partial derivative of a kernel in the coordinate direction j.

Equations

• CKN.vlDeriv k j y = (fderiv ℝ k y) (CKN.basisVec j)

def CKN.IsVlKernel (k : Foundation.Parabolic.Vec3 → ℝ) : Prop

Smooth compactly supported kernels.

Equations

• CKN.IsVlKernel k = (ContDiff ℝ (↑⊤) k ∧ HasCompactSupport k)

theorem CKN.vlConv_apply (k h : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) : vlConv k h x = ∫ (t : Foundation.Parabolic.Vec3), k t * h (x - t)

theorem CKN.IsVlKernel.continuous {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) : Continuous k

theorem CKN.IsVlKernel.integrable {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) : MeasureTheory.Integrable k MeasureTheory.volume

theorem CKN.IsVlKernel.deriv {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (j : Fin 3) : IsVlKernel (vlDeriv k j)

theorem CKN.IsVlKernel.sub {k l : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hl : IsVlKernel l) : IsVlKernel (k - l)

theorem CKN.IsVlKernel.smul {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (c : ℝ) : IsVlKernel (c • k)

theorem CKN.vlDeriv_sub {k l : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hl : IsVlKernel l) (j : Fin 3) : vlDeriv (k - l) j = vlDeriv k j - vlDeriv l j

theorem CKN.vlConv_contDiff {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) : ContDiff ℝ (↑⊤) (vlConv k h)

The convolution of a locally integrable field with a smooth compact kernel is smooth.

theorem CKN.vlConv_fderiv_apply {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (j : Fin 3) : (fderiv ℝ (vlConv k h) x) (basisVec j) = vlConv (vlDeriv k j) h x

Differentiating a convolution differentiates the kernel.

theorem CKN.vlConv_partial {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) (j : Fin 3) : vlDeriv (vlConv k h) j = vlConv (vlDeriv k j) h

The convolution partial derivative, in CKN notation.

theorem CKN.vlConv_continuous {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) : Continuous (vlConv k h)

theorem CKN.vlConv_eLpNorm_le {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (vlConv k h) 2 MeasureTheory.volume ≤ ENNReal.ofReal (∫ (y : Foundation.Parabolic.Vec3), |k y|) * MeasureTheory.eLpNorm h 2 MeasureTheory.volume

Young's inequality in L² for a smooth compact kernel of any sign.

theorem CKN.vlConv_memLp {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : MeasureTheory.MemLp (vlConv k h) 2 MeasureTheory.volume

theorem CKN.vlConv_integral_mul_deriv {k l h₁ h₂ : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hl : IsVlKernel l) (hh₁ : MeasureTheory.MemLp h₁ 2 MeasureTheory.volume) (hh₂ : MeasureTheory.MemLp h₂ 2 MeasureTheory.volume) (j : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), vlConv k h₁ x * vlConv (vlDeriv l j) h₂ x = -∫ (x : Foundation.Parabolic.Vec3), vlConv (vlDeriv k j) h₁ x * vlConv l h₂ x

Integration by parts for kernel convolutions of L² fields.

theorem CKN.vlConv_sub_kernel {k l h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hl : IsVlKernel l) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) : vlConv (k - l) h = vlConv k h - vlConv l h

Convolution is linear in the kernel.