Component bounds for the regularized convolution

The finite-dimensional coordinate decomposition transfers scalar slice estimates through the vector-valued mollifier.

theorem CKN.Leray.regMollifyVector_component_eLpNorm_le_sum (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {p : ENNReal} (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hu₂ : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hup : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x j) p MeasureTheory.volume) (i : Fin 3) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => (regMollifyVector ρ ε hε (regUniformSpatialField u) (WithLp.toLp 2 x)).ofLp i) p MeasureTheory.volume ≤ ∑ j : Fin 3, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x j) p MeasureTheory.volume

Convolution by the regularizing profile does not increase a scalar component's L^p norm beyond the sum of the input component norms.