The weak momentum equation for the Leray–Hopf limit

This is the weak-equation clause (LH3) of def:leray-hopf in the proof of prop:leray-hopf-limit. For a solenoidal test supported in ℝ³ × (0,T), the regularized identity of lem:reg-momentum has no pressure term. On the compact support of the test, strong L³ convergence of the velocities and of their mollifications and weak L² convergence of the gradients pass every term to the limit.

theorem CKN.Leray.lerayHopfLimit_compact_time_bounds {T : ℝ} (hT : 0 < T) {K : Set (Foundation.Parabolic.Vec3 × ℝ)} (hK : IsCompact K) (hKsub : K ⊆ Set.univ ×ˢ Set.Ioo 0 T) : ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ K ⊆ Set.univ ×ˢ Set.Ioo δ T

A compact subset of a finite positive-time slab stays a positive distance away from the initial time.

theorem CKN.Leray.lerayHopfLimit_momentum (T : ℝ) (hT : 0 < T) (U J : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (P : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hU3 : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hJ3 : ∀ (n : ℕ), MeasureTheory.MemLp (J n) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hu3 : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDweak : ∀ (i j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U n y i) j z * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), Du z i j * w z))) (hDloc : ∀ (δ : ℝ), 0 < δ → δ < T → ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U n y i) j z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) (hreg : ∀ (n : ℕ), ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, U n z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, J n z j * U n z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => U n y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - P n z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) (φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T) → (∀ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) → ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z = 0

The weak momentum clause (LH3) for the limit of regularized solutions.