Forced Leray Limit Prop J

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.forcedLerayLimit_mollified_convergence_of_strong_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) (hUmeas : ∀ (n : ℕ), Measurable (U n)) (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)

Strong L³ convergence of the regularized velocities implies strong L³ convergence of their spatially mollified transports.