Compactness Local

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.strong_l2_on_compact_rectangle_of_cutoff_weak_slices {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hU : IsOpen U) (hI : IsOpen I) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (hDuMeas : ∀ (n : ℕ), Measurable (Du n)) (hweakGrad : ∀ (n : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u n (x, t) i) fun (x : Vec 3) => Du n (x, t) i) (hbound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (J : Set ℝ), IsCompact J → J ⊆ I → ∃ M < ⊤, ∀ (n : ℕ), ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) (hgradBound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (J : Set ℝ), IsCompact J → J ⊆ I → ∃ G < ⊤, ∀ (n : ℕ), ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1))) (hKcover : ⋃ (j : ℕ), K j = U) (hχ : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (χ j) ∧ HasCompactSupport (χ j) ∧ tsupport (χ j) ⊆ U ∧ (∀ (x : Foundation.Parabolic.Vec3), χ j x ∈ Set.Icc 0 1) ∧ ∀ x ∈ K j, χ j x = 1) (hmem : ∀ (n j : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ j x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume) (σ : ℕ → ℕ) (V : ℕ → ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (j : ℕ) (t : ↑I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ j y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V j t) x))) (hVcont : ∀ (j : ℕ) (x : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)), Continuous fun (t : ↑I) => inner ℝ (V j t) x) (huniform : ∀ (j : ℕ) (p : RationalCompactTimeWindow I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)) (ε : ℝ), 0 < ε → ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (t : RationalTimeSlice p), dist (inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ j y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) (inner ℝ (V j ⟨↑t, ⋯⟩) x) < ε) {C : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hC : IsCompact C) (hCU : C ⊆ U) (hJ : IsCompact J) (hJI : J ⊆ I) : ∃ (hf : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) 2 ((MeasureTheory.volume.restrict C).prod (MeasureTheory.volume.restrict J))) (g : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 ((MeasureTheory.volume.restrict C).prod (MeasureTheory.volume.restrict J)))), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) ⋯) Filter.atTop (nhds g)

The common weak slice extraction and the local energy bounds give strong L² convergence on every compact space-time rectangle.