Compactness Strong Identification #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.strong_product_limit_ae_eq_of_weak_slices
{K : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
[MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict K)]
(hJ : MeasurableSet J)
(f : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3)
(u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3)
(hu : Measurable u)
(hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)))
(G :
↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2
((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))))
(hstrong : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (f n) ⋯) Filter.atTop (nhds G))
(hfslice :
∀ (n : ℕ),
∀ t ∈ J,
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f n (x, t)) 2 (MeasureTheory.volume.restrict K))
(huslice :
∀ t ∈ J, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 (MeasureTheory.volume.restrict K))
(hweak :
∀ (t : ℝ) (ht : t ∈ J) (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict K))),
Filter.Tendsto
(fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => f n (x, t)) ⋯) w)
Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯) w)))
(hbound :
∃ B < ⊤,
∀ (n : ℕ),
∀ t ∈ J,
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f n (x, t)) 2 (MeasureTheory.volume.restrict K) ≤ B)
:
(fun (z : Foundation.Parabolic.Vec3 × ℝ) =>
↑↑G z) =ᵐ[(MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)]
u
A local strong space-time limit is the jointly measurable representative of the all-time weak slice limit.