Convolution with continuous compactly supported kernels on L²(ℝ³)

Scalar facts behind the Leray projection of prop:lps-smoothing: convolution with a continuous compactly supported kernel is bounded on L², its L² adjoint is convolution with the reflected kernel, it maps test functions to test functions commuting with partial derivatives, and a weak derivative of the convolved function can be moved onto a smooth kernel.

theorem ESS.lpsLeray_conv_apply (θ f : CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) : MeasureTheory.convolution θ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = ∫ (t : CKN.Foundation.Parabolic.Vec3), θ t * f (x - t)

Pointwise formula for real convolution (prop:lps-smoothing).

theorem ESS.lpsLeray_eLpNorm_conv_le {θ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (MeasureTheory.convolution θ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) 2 MeasureTheory.volume ≤ ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), ‖θ x‖) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Convolution with a continuous compactly supported kernel is bounded on L²(ℝ³): ‖θ ⋆ f‖₂ ≤ ‖θ‖₁ ‖f‖₂ (prop:lps-smoothing).

theorem ESS.lpsLeray_memLp_conv {θ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (MeasureTheory.convolution θ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) 2 MeasureTheory.volume

Convolution with a continuous compactly supported kernel preserves L²(ℝ³) (prop:lps-smoothing).

theorem ESS.lpsLeray_integral_conv_mul_eq {θ f h : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), MeasureTheory.convolution θ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x * h x = ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * MeasureTheory.convolution (fun (y : CKN.Foundation.Parabolic.Vec3) => θ (-y)) h (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The L² adjoint of convolution with θ is convolution with the reflected kernel x ↦ θ (-x) (prop:lps-smoothing).

theorem ESS.lpsLeray_conv_spatialDeriv_kernel {η g G : CKN.Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hg : CKN.HasWeakPartialDerivOn Set.univ k g G) (x : CKN.Foundation.Parabolic.Vec3) : MeasureTheory.convolution (CKN.spatialDeriv η k) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = MeasureTheory.convolution η G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Moving a weak derivative onto a smooth compactly supported kernel: (∂_k η) ⋆ g = η ⋆ G when G is the weak k-th derivative of g (prop:lps-smoothing).

theorem ESS.lpsLeray_spatialDeriv_reflect {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Differentiable ℝ θ) (k : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => θ (-y)) k x = -CKN.spatialDeriv θ k (-x)

The partial derivative of a reflected kernel (prop:lps-smoothing).

theorem ESS.lpsLeray_spatialDeriv_conv_test {θ φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.spatialDeriv (MeasureTheory.convolution θ φ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) i x = MeasureTheory.convolution θ (CKN.spatialDeriv φ i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Convolving a test function with a continuous kernel commutes with partial derivatives (prop:lps-smoothing).

theorem ESS.lpsLeray_contDiff_conv_test {θ φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ContDiff ℝ (↑⊤) (MeasureTheory.convolution θ φ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

Convolving a test function with a continuous compactly supported kernel gives a test function (prop:lps-smoothing).

theorem ESS.lpsLeray_hasCompactSupport_conv {θ φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθc : HasCompactSupport θ) (hφc : HasCompactSupport φ) : HasCompactSupport (MeasureTheory.convolution θ φ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

Convolution of two compactly supported functions is compactly supported (prop:lps-smoothing).