Compactness Gradient Compatibility

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.weak_partial_representatives_agree_on_nested_rectangles (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (hKmono : ∀ (j : ℕ), K j ⊆ K (j + 1)) (hJmono : ∀ (j : ℕ), J j ⊆ J (j + 1)) (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (g : ℕ → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hgMeas : ∀ (j : ℕ), Measurable (g j)) (m : Fin 3) (hlocal : ∀ (j : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (J j), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => g j (x, t)) (interior (K j)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (interior (K j)) m (fun (x : Vec 3) => f (x, t)) fun (x : Vec 3) => g j (x, t)) {a b : ℕ} (hab : a ≤ b) : g a =ᵐ[(MeasureTheory.volume.restrict (interior (K a))).prod (MeasureTheory.volume.restrict (J a))] g b

Locally integrable representatives of the same weak spatial derivative agree almost everywhere on nested open space-time rectangles.