Compactness Gradient Global

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_measurable_gradient_of_local_weak_partials (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (hKmono : ∀ (j : ℕ), K j ⊆ K (j + 1)) (hJmono : ∀ (j : ℕ), J j ⊆ J (j + 1)) (hJ : ∀ (j : ℕ), IsCompact (J j)) (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (gLocal : ℕ → Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber) (hgMeas : ∀ (j : ℕ), Measurable (gLocal j)) (hlocal : ∀ (j : ℕ) (i m : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (J j), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => ((gLocal j (x, t)).ofLp i).ofLp m) (interior (K j)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (interior (K j)) m (fun (x : Vec 3) => u (x, t) i) fun (x : Vec 3) => ((gLocal j (x, t)).ofLp i).ofLp m) : ∃ (g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber), Measurable g ∧ ∀ (j : ℕ), g =ᵐ[(MeasureTheory.volume.restrict (interior (K j))).prod (MeasureTheory.volume.restrict (J j))] gLocal j

Compatible local weak spatial gradients on a nested exhaustion have a jointly measurable representative that agrees with each local gradient almost everywhere on its full open rectangle.