Compactness Gradient Weak Local

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.weak_gradient_to_measurable_limit_on_compact {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → 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) (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))) (g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber) (hgEq : ∀ (j : ℕ), g =ᵐ[(MeasureTheory.volume.restrict (interior (K j))).prod (MeasureTheory.volume.restrict (J j))] compactnessGradientLocalRepresentative K J D j) (Q : Set (Foundation.Parabolic.Vec3 × ℝ)) (hQ : IsCompact Q) (hQI : Q ⊆ U ×ˢ I) : ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) 2 (MeasureTheory.volume.restrict Q)) (hl : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict Q)), ∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 (MeasureTheory.volume.restrict Q))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp g hl) w))

The jointly measurable gradient limit is the weak local L² limit of the selected matrix gradients on every compact space-time set.