Compactness Gradient Limit

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.compactness_gradient_limit_of_joint_limits {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hU : IsOpen U) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1))) (hKcover : ⋃ (j : ℕ), K j = U) (hJ : ∀ (j : ℕ), IsCompact (J j) ∧ J j ⊆ I ∧ J j ⊆ J (j + 1) ∧ J j ⊆ interior (J (j + 1))) (hJcover : ⋃ (j : ℕ), J j = I) (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) (D : (j : ℕ) → ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))) (hDweak : ∀ (j : ℕ), ∃ (hgrad : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))), ∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) ⋯) w) Filter.atTop (nhds (inner ℝ (D j) w))) (hstrong : ∀ (j : ℕ), ∃ (_ : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm ((fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) - fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (v z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))) Filter.atTop (nhds 0)) : ∃ (g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber), Measurable g ∧ (∀ (j : ℕ), g =ᵐ[(MeasureTheory.volume.restrict (interior (K j))).prod (MeasureTheory.volume.restrict (J j))] compactnessGradientLocalRepresentative K J D j) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => v (x, t) i) fun (x : Vec 3) (m : Fin 3) => ((g (x, t)).ofLp i).ofLp m

Strong local velocity convergence and weak local matrix convergence select a measurable limit gradient with the almost-every-time weak spatial-gradient identity on the full open domain.