Leray Limit Slice Bridge #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.lerayLimit_globalSlices_of_localWeak
(F : ℕ → ℝ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(u : ℝ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(K : ℕ → Set Foundation.Parabolic.Vec3)
(hK : MeasureTheory.AECover MeasureTheory.volume Filter.atTop K)
(C : ℝ)
(hC : 0 ≤ C)
(hFmeas : ∀ (n : ℕ) (t : ℝ), Measurable fun (x : Foundation.Parabolic.Vec3) => F n t x)
(humeas : ∀ (t : ℝ), Measurable fun (x : Foundation.Parabolic.Vec3) => u t x)
(hFbound :
∀ (t : ℝ) (n k : ℕ),
∫⁻ (x : Foundation.Parabolic.Vec3) in K k, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (F n t x)) ^ 2 ≤ ENNReal.ofReal C ^ 2)
(hubound :
∀ (t : ℝ),
0 < t →
∀ (k : ℕ),
∫⁻ (x : Foundation.Parabolic.Vec3) in K k, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u t x)) ^ 2 ≤ ENNReal.ofReal C ^ 2)
(hlocal :
∀ (t : ℝ),
0 < t →
∀ (v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3),
HasCompactSupport v →
Continuous v →
∀ (hv : MeasureTheory.MemLp v 2 MeasureTheory.volume)
(hF :
∀ (n : ℕ),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n t x)) 2
MeasureTheory.volume)
(hu :
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) 2
MeasureTheory.volume),
Filter.Tendsto
(fun (n : ℕ) =>
inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n t x)) ⋯)
(MeasureTheory.MemLp.toLp v hv))
Filter.atTop
(nhds
(inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) hu)
(MeasureTheory.MemLp.toLp v hv))))
(t : ℝ)
(ht : 0 < t)
:
∃ (hF :
∀ (n : ℕ),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n t x)) 2 MeasureTheory.volume)
(hu : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) 2 MeasureTheory.volume),
(∀ (n : ℕ), ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n t x)) ⋯‖ ≤ C) ∧ ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) hu‖ ≤ C ∧ ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3)
(hw : MeasureTheory.MemLp w 2 MeasureTheory.volume),
Filter.Tendsto
(fun (n : ℕ) =>
inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n t x)) ⋯)
(MeasureTheory.MemLp.toLp w hw))
Filter.atTop
(nhds
(inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) hu)
(MeasureTheory.MemLp.toLp w hw)))
Local every-time weak limits and uniform energy bounds give global L² slices and global weak convergence on every positive-time slice.