Compactness Fixed Rank

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.tendsto_finite_rank_ball_average_approximation {ι : Type u_1} [Fintype ι] {I J : Set ℝ} {K : Set Foundation.Parabolic.Vec3} (hJI : J ⊆ I) (hK : MeasurableSet K) (hJ : MeasurableSet J) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict K)] [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (B : ι → Set Foundation.Parabolic.Vec3) (hB : ∀ (i : ι), MeasurableSet (B i)) (hBfinite : ∀ (i : ι), MeasureTheory.volume (B i) < ⊤) (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ (i : ι), ∀ x ∈ B i, χ x = 1) (hmem : ∀ (n : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (t : ↑I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V t) x))) (hVcont : ∀ (x : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)), Continuous fun (t : ↑I) => inner ℝ (V t) x) (huniform : ∀ (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ℝ) (ht : t ∈ J), dist (inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, t))) ⋯) x) (inner ℝ (V ⟨t, ⋯⟩) x) < ε) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (n : ℕ) (t : ℝ) (ht : t ∈ J), ‖MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, t))) ⋯‖ ≤ C) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (hφ : ∀ (i : ι), Measurable (φ i)) (hφbound : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), |φ i x| ≤ 1) : ∃ (hP : ∀ (n : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • fun (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in B i, u n (y, z.2) j)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (Q : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3) (hQ : MeasureTheory.MemLp Q 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • fun (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in B i, u n (y, z.2) j)) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp Q hQ))

At a fixed finite spatial rank, weak convergence of cutoff slices makes the ball-average approximants converge strongly on a compact rectangle.