The L³ contraction of the regularized transport velocity

The transport velocity J_ε u of thm:regularised is, on each time slice, the convolution of the slice with the normalized dilate of the regularizing profile, written in coordinates. Convolution with a nonnegative kernel of unit mass is contractive in every finite Lebesgue norm, slice by slice; integrating in time gives the space-time contraction used for the L³ assertion of prop:leray-limit.

theorem CKN.Leray.lerayLimit_regMollifierKernel_vec3_props (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : (∀ (y : Foundation.Parabolic.Vec3), 0 ≤ regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) ∧ (Continuous fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) ∧ MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) MeasureTheory.volume ∧ ∫ (y : Foundation.Parabolic.Vec3), regMollifierKernel ρ ε hε (WithLp.toLp 2 y) = 1 ∧ (Function.support fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) ⊆ Metric.ball 0 ε ∧ HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)

The regularizing kernel in coordinates is a nonnegative, continuous, compactly supported kernel of unit mass supported in the ball of radius ε.

theorem CKN.Leray.lerayLimit_regUniformMollifiedVelocity_eq_convolution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x : Foundation.Parabolic.Vec3) (t : ℝ) : regUniformMollifiedVelocity ρ ε hε v (x, t) = MeasureTheory.convolution (fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) (fun (y : Foundation.Parabolic.Vec3) => v (y, t)) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

On each time slice, the regularized transport velocity is the coordinate convolution of the slice with the regularizing kernel.

theorem CKN.Leray.lerayLimit_regMollifierKernel_convolution_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (x : Foundation.Parabolic.Vec3) : ‖MeasureTheory.convolution (fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x‖ ≤ MeasureTheory.convolution (fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) (fun (y : Foundation.Parabolic.Vec3) => ‖f y‖) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Convolution with the coordinate regularizing kernel is dominated pointwise by the convolution of the norm.

theorem CKN.Leray.lerayLimit_regUniformMollifiedVelocity_slice_eLpNorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hu : MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) MeasureTheory.volume) {p : ENNReal} (hp : 1 ≤ p) (hpTop : p ≠ ⊤) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t)) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) p MeasureTheory.volume

On each time slice, the regularized transport velocity has finite-exponent Lebesgue norm at most that of the slice itself.

theorem CKN.Leray.lerayLimit_regUniformMollifiedVelocity_stronglyMeasurable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hv : Measurable v) : MeasureTheory.StronglyMeasurable (regUniformMollifiedVelocity ρ ε hε v)

The regularized transport velocity of a measurable space-time field is strongly measurable.

theorem CKN.Leray.lerayLimit_regUniformMollifiedVelocity_spaceTime_eLpNorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hv : Measurable v) (T : ℝ) : MeasureTheory.eLpNorm (regUniformMollifiedVelocity ρ ε hε v) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ MeasureTheory.eLpNorm v 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))

Integrating the per-time contraction over a time slab gives the space-time L³ contraction of the regularized transport velocity.