The regularized transport field on space-time slabs

The transport velocity J_ε u of the forced regularized problem (lem:regularised-forced) is, on every time slice, the convolution of the velocity slice with the smooth compactly supported regularizing kernel. For a jointly measurable velocity with square-integrable slices it is therefore jointly measurable, and the slice contraction of the convolution in L^p (lem:reg-mollifier-bounds) integrates in time to a space-time L^p bound on every slab, as used in lem:forced-energy-bounds.

theorem CKN.Leray.forcedLerayLimit_transport_component_eq (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (hz : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, z.2)) 2 MeasureTheory.volume) (i : Fin 3) : regUniformMollifiedVelocity ρ ε hε u z i = ∫ (y : Foundation.Parabolic.Vec3), forcedTransportKernel ρ ε hε y * u (z.1 - y, z.2) i

On each slice with square-integrable velocity, the regularized transport velocity is the kernel convolution of the velocity components.

theorem CKN.Leray.forcedLerayLimit_transport_measurable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hu : MeasureTheory.StronglyMeasurable u) (hslice : ∀ (t : ℝ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) : Measurable (regUniformMollifiedVelocity ρ ε hε u)

The regularized transport velocity of a jointly measurable velocity with square-integrable slices is jointly measurable.

theorem CKN.Leray.forcedLerayLimit_transport_eLpNorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hu : MeasureTheory.StronglyMeasurable u) (hslice : ∀ (t : ℝ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) {p : ENNReal} (hp : 1 ≤ p) (hptop : p ≠ ⊤) (I : Set ℝ) (i : Fin 3) : MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u z i) p (MeasureTheory.volume.restrict (spaceTimeSet Set.univ I)) ^ p.toReal ≤ 3 ^ (p.toReal - 1) * ∑ j : Fin 3, MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) p (MeasureTheory.volume.restrict (spaceTimeSet Set.univ I)) ^ p.toReal

The space-time L^p bound of the regularized transport velocity on a slab over a time set I: each component is controlled by the three velocity components, uniformly in the regularization parameter.