Pointwise bound for complex Schwartz mollification

The convolution of the fixed Schwartz kernel with an L² Schwartz velocity is bounded at each spatial point by the L² Hölder estimate.

theorem CKN.Leray.regularisedSchwartzMollify_enorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : ‖(regularisedSchwartzMollify ρ ε hε ψ) x‖ₑ ≤ ‖ContinuousLinearMap.lsmul ℂ ℂ‖ₑ * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.L2Vec3) => ↑(regMollifierKernel ρ ε hε y)) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑ψ) 2 MeasureTheory.volume

Complex Schwartz mollification obeys the L²-by-L² pointwise convolution bound.

theorem CKN.Leray.regularisedSchwartzMollify_enorm_le_kernel (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : ‖(regularisedSchwartzMollify ρ ε hε ψ) x‖ₑ ≤ MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.L2Vec3) => ↑(regMollifierKernel ρ ε hε y)) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑ψ) 2 MeasureTheory.volume

Complex Schwartz mollification has pointwise bound with the exact L² kernel factor, since scalar multiplication has bilinear norm one.

theorem CKN.Leray.regularisedSchwartzMollify_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3), ‖(regularisedSchwartzMollify ρ ε hε ψ) x‖ ≤ C * ‖ψ.toLp 2 MeasureTheory.volume‖

One finite constant, fixed by the mollifier and scale, bounds complex Schwartz mollification pointwise by the input L² norm.