Leray Hopf Limit Prop LH1

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayHopfLimit_LH1_of_limitData (T : ℝ) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ρ : RegMollifierProfile) (εseq : ℕ → ℝ) (σ : ℕ → ℕ) (hεpositive : ∀ (n : ℕ), 0 < εseq (σ n)) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Dseq : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (humeas : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDmeas : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hgradient : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => Du (x, s) i) (hdivU : ∀ (n : ℕ) (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => U n (x, t)) (hweakSlice : ∀ (t : ℝ), 0 < t → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U n (x, t) i * w x i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) (hsliceU : ∀ (n : ℕ) (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => U n (x, t)) 2 MeasureTheory.volume) (hR5 : ∀ (n : ℕ) (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice (U n) t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation (U n) (Dseq n) t = MeasureTheory.eLpNorm (regMollifyVector ρ (εseq (σ n)) ⋯ (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2) : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ essSup (fun (s : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ‖u (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤ ∧ ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤ ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => Du (x, s) i) ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (ψ : WeakTestFunction Set.univ), ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i * ψ.partialDeriv i x = 0

All six (LH1) properties follow from the slab limit fields, the global weak slice convergence, the exact regularized energy identity, and its regularized divergence-free slices.