Strong L³ convergence of the regularized transport velocities

In prop:leray-limit the transport velocities J_{ε_n} u_{ε_n} converge to the limit velocity strongly in L³ on every finite slab. The argument approximates the limit by a continuous compactly supported field, on which the regularization converges uniformly with supports in a fixed compact set, and controls the remaining terms by the space-time L³ contraction and the strong L³ convergence of the velocities themselves.

theorem CKN.Leray.lerayLimit_regUniformMollifiedVelocity_tendsto_of_compact (ρ : RegMollifierProfile) (T : ℝ) (g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hg : Continuous g) (hgc : HasCompactSupport g) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hlim : Filter.Tendsto ε Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((regUniformMollifiedVelocity ρ (ε n) ⋯ fun (z : Foundation.Parabolic.ParabolicPoint) => g (z.1, z.2)) - fun (z : Foundation.Parabolic.ParabolicPoint) => g (z.1, z.2)) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)

For a continuous compactly supported space-time field, the regularized transport velocities converge to the field in L³ on a finite slab.

theorem CKN.Leray.lerayLimit_regUniformMollifiedVelocity_tendsto_three (ρ : RegMollifierProfile) (T : ℝ) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hlim : Filter.Tendsto ε Filter.atTop (nhds 0)) (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hUcont : ∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => U n z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hUslice : ∀ (n : ℕ) (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => U n (x, t)) 2 MeasureTheory.volume) (hU3 : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) : (∀ (n : ℕ), MeasureTheory.MemLp (regUniformMollifiedVelocity ρ (ε n) ⋯ (U n)) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) ∧ MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (regUniformMollifiedVelocity ρ (ε n) ⋯ (U n) - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)

The L³ assertion of prop:leray-limit for the transport velocities: from the strong L³ convergence of the regularized velocities on a finite slab, the regularized transport velocities are cubically integrable there, the limit is cubically integrable, and the transport velocities converge to the limit in L³.