Uniform pointwise estimate for Schwartz convolution

An arbitrary scalar Schwartz kernel acts from vector L² to bounded continuous vector fields with a bound determined by its L² norm.

theorem CKN.Leray.regularised_schwartz_convolution_norm_le (κ : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : ‖(((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) κ) ψ) x‖ ≤ ‖κ.toLp 2 MeasureTheory.volume‖ * ‖ψ.toLp 2 MeasureTheory.volume‖

Convolution of a complex scalar Schwartz kernel with a complex vector Schwartz field is pointwise bounded by the product of their L² norms.