Compactness Representative AE

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.compactnessMollifiedLimit_ae_eq_weak_slice_on {I : Set ℝ} {K : Set Foundation.Parabolic.Vec3} (hK : MeasurableSet K) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hfixed : ∀ (t : ↑I), ∀ x ∈ K, ∀ (i : Fin 3), ∀ᶠ (m : ℕ) in Filter.atTop, (Filter.atTop.limUnder fun (k : ℕ) => mollify (fun (y : Foundation.Parabolic.Vec3) => u (σ k) (y, ↑t) i) (sliceRadius m) ⋯ x) = mollify (fun (y : Foundation.Parabolic.Vec3) => (↑↑(V t) y).ofLp i) (sliceRadius m) ⋯ x) (t : ↑I) : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict K, compactnessMollifiedLimit u σ (x, ↑t) = fun (i : Fin 3) => (↑↑(V t) x).ofLp i

Eventual fixed-scale identification with mollifications of an L² slice identifies the measurable limit with that slice almost everywhere.