Leray Assembly Hopf Data

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayAssembly_productSlab_memLp_to_parabolic {T : ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} {r : ENNReal} (hf : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => f (Foundation.Parabolic.parabolicHomeomorph.symm z)) r (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) : MeasureTheory.MemLp f r (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))

Pull back finite-slab pressure integrability from product coordinates to CKN's parabolic-point coordinates.

theorem CKN.Leray.lerayAssembly_pressureConv_localBox {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {T : ℝ} (hbox : localBox Set.univ (Set.Ioi 0) Ω' J) (hJT : J ⊆ Set.Ioo 0 T) (pseq : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hpseq : ∀ (n : ℕ), MeasureTheory.MemLp (pseq n) 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hp : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => p (Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => pseq n (Foundation.Parabolic.parabolicHomeomorph.symm z) - p (Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (pseq n - p) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)

Strong pressure convergence on the product slab restricts to, and agrees with, convergence on a compact parabolic test box.

theorem CKN.Leray.lerayAssembly_localBox_time_bounds {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Set.univ (Set.Ioi 0) Ω' J) : ∃ (δ : ℝ) (T : ℝ), 0 < δ ∧ δ < T ∧ J ⊆ Set.Ioo δ T

A local box compactly contained in positive time is contained in a strictly positive finite open time slab.

theorem CKN.Leray.lerayAssembly_strongConv_localBox {E : Type u_1} [NormedAddCommGroup E] {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {T : ℝ} {r : ENNReal} (hJ : J ⊆ Set.Ioo 0 T) (F : ℕ → Foundation.Parabolic.ParabolicPoint → E) (f : Foundation.Parabolic.ParabolicPoint → E) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) r (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) r (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)

Strong convergence on a finite positive-time slab restricts to each local box inside that slab.

theorem CKN.Leray.lerayAssembly_weakConv_localBox {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {T : ℝ} (hJ : J ⊆ Set.Ioo 0 T) (F : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (f w : Foundation.Parabolic.ParabolicPoint → ℝ) (hwzero : ∀ z ∉ spaceTimeSet Ω' J, w z = 0) (hweak : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), F n z * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z * w z))) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, F n z * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, f z * w z))

Weak gradient pairings on a slab restrict to a test supported in a local box.

theorem CKN.Leray.lerayAssembly_weakConv_localBox_all {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {T : ℝ} (hbox : localBox Set.univ (Set.Ioi 0) Ω' J) (hJ : J ⊆ Set.Ioo 0 T) (F : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → ℝ) (hweak : ∀ (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), F n z * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z * w z))) (w : Foundation.Parabolic.ParabolicPoint → ℝ) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, F n z * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, f z * w z))

Weak slab convergence gives every local-box weak pairing by extending the local test by zero.

theorem CKN.Leray.lerayAssembly_regMomentum_localBox {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) (hKbox : tsupport (have this := φ; this) ⊆ spaceTimeSet Ω' J) (U Jv : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, U z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, Jv z j * U z i * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, D z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, -∑ i : Fin 3, U z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, Jv z j * U z i * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, D z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z

The regularized momentum pairing is supported in the test field's compact support.

theorem CKN.Leray.lerayAssembly_hopfData {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hglobal : ∀ (T : ℝ), 0 < T → IsLerayHopfSolution T a u Du) (hp : ∀ (T : ℝ), 0 < T → MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) {q : ℝ} (hq : 5 / 2 < q) : IsSuitableWeakSolutionData Set.univ (Set.Ioi 0) q u Du p 0

A global Leray--Hopf pair and its finite-slab pressure integrability give the data clauses of def:sws on the positive-time half space.

theorem CKN.Leray.lerayAssembly_hopfDivergence {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hglobal : ∀ (T : ℝ), 0 < T → IsLerayHopfSolution T a u Du) (ψ : Foundation.Parabolic.ParabolicPoint → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0

The divergence identity on positive time follows from the every-slab Leray--Hopf weak-divergence clause.