Compactness Approximation

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_finite_rank_average_approximation_of_mixed_bounds {K W Kc : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) (hWKc : W ⊆ Kc) (hJ : MeasurableSet J) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (hDuMeas : ∀ (n : ℕ), Measurable (Du n)) (hweak : ∀ (n : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn W (fun (y : Vec 3) => u n (y, t) i) fun (y : Vec 3) => Du n (y, t) i) (M G : ENNReal) (hM : M < ⊤) (hG : G < ⊤) (huBound : ∀ (n : ℕ), ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) (hDuBound : ∀ (n : ℕ), ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) (ε : ENNReal) : 0 < ε → ∃ (m : ℕ) (N : ℕ) (s : Fin N → Set { x : Foundation.Parabolic.Vec3 // x ∈ K }) (t : Finset ((i : Fin N) × { x : { x : Foundation.Parabolic.Vec3 // x ∈ K } // x ∈ s i })) (φ : ↥t → Foundation.Parabolic.Vec3 → ℝ), (∀ (p : ↥t), Measurable (φ p)) ∧ (∀ (p : ↥t) (y : Foundation.Parabolic.Vec3), 0 ≤ φ p y ∧ φ p y ≤ 1) ∧ (∀ (p : ↥t), euclideanBall (↑↑(↑p).snd) (1 / (↑m + 1)) ⊆ W) ∧ ∀ (n : ℕ), ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n z - ∑ p : ↥t, φ p z.1 • fun (j : Fin 3) => ⨍ (y : Vec 3) in euclideanBall (↑↑(↑p).snd) (1 / (↑m + 1)), u n (y, z.2) j) ^ 2) ≤ ε

The local slice and integrated gradient bounds give finite-rank spatial approximations with uniformly small space-time error.