Compactness Gradient Time Glue #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.ae_weak_partial_on_union_of_exhaustions
{U : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hU : IsOpen U)
(K : ℕ → Set Foundation.Parabolic.Vec3)
(J : ℕ → Set ℝ)
(hKmono : ∀ (j : ℕ), K j ⊆ K (j + 1))
(hKinner : ∀ (j : ℕ), K j ⊆ interior (K (j + 1)))
(hKcover : ⋃ (j : ℕ), K j = U)
(hJmono : ∀ (j : ℕ), J j ⊆ J (j + 1))
(hJcover : ⋃ (j : ℕ), J j = I)
(f d : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(m : Fin 3)
(hlocal :
∀ (j : ℕ),
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (J j), HasWeakPartialDerivOn (interior (K j)) m (fun (x : Vec 3) => f (x, t)) fun (x : Vec 3) => d (x, t))
:
Almost-every-time weak spatial derivatives on a nested product exhaustion give one almost-every-time weak derivative on the full open spatial domain.