Finite-exponent contraction for the regularizing convolution

The convolution by the normalized nonnegative kernel is contractive on every finite spatial L^p space on which the input also has the L² regularity needed to define its Bochner convolution.

noncomputable def CKN.Leray.regUniformProfileOnVec3 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.Vec3 → ℝ

The regularized radial profile written as a function on native three-dimensional coordinates.

Equations

• CKN.Leray.regUniformProfileOnVec3 ρ ε hε x = CKN.Leray.regMollifierKernel ρ ε hε (WithLp.toLp 2 x)

noncomputable def CKN.Leray.regUniformL2VectorNormOnVec3 (f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) : Foundation.Parabolic.Vec3 → ℝ

The pointwise norm of a spatial L² vector field in Euclidean coordinates.

Equations

• CKN.Leray.regUniformL2VectorNormOnVec3 f x = ‖f (WithLp.toLp 2 x)‖

noncomputable def CKN.Leray.regUniformConvolutionMajor (f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.L2Vec3 → ℝ

The coordinate-space norm profile used to dominate the regularized convolution uniformly.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regMollifyVector_eLpNorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) {p : ENNReal} (hp : 1 ≤ p) (hpTop : p ≠ ⊤) : MeasureTheory.eLpNorm (regMollifyVector ρ ε hε f) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm (regUniformL2VectorNormOnVec3 f) p MeasureTheory.volume

Normalized regularizing convolution is contractive at any finite exponent p ≥ 1, provided its input also lies in L².