Compactness Gradient Glue

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.hasWeakPartialDerivOn_of_inner_exhaustion {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) (K : ℕ → Set Foundation.Parabolic.Vec3) (hKmono : ∀ (j : ℕ), K j ⊆ K (j + 1)) (hKinner : ∀ (j : ℕ), K j ⊆ interior (K (j + 1))) (hKcover : ⋃ (j : ℕ), K j = U) (f d : Foundation.Parabolic.Vec3 → ℝ) (i : Fin 3) (hlocal : ∀ (j : ℕ), HasWeakPartialDerivOn (interior (K j)) i f d) : HasWeakPartialDerivOn U i f d

Weak spatial derivatives on every open inner member of a compact exhaustion give the weak derivative on the whole open domain.

theorem CKN.Leray.ae_eq_on_nested_sets_of_disjointed_representative {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (R : ℕ → Set α) (hRmeas : ∀ (j : ℕ), MeasurableSet (R j)) (g : ℕ → α → E) (F : α → E) (hF : ∀ (j : ℕ), Set.EqOn F (g j) (disjointed R j)) (hcompat : ∀ (i j : ℕ), i ≤ j → g i =ᵐ[μ.restrict (R i)] g j) (j : ℕ) : F =ᵐ[μ.restrict (R j)] g j

A measurable field assembled on disjointed nested sets agrees almost everywhere with each compatible local representative on its full set.

theorem CKN.Leray.exists_measurable_disjointed_gradient_representative (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (hJ : ∀ (j : ℕ), IsCompact (J j)) (gLocal : ℕ → Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber) (hgMeas : ∀ (j : ℕ), Measurable (gLocal j)) : ∃ (g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber), Measurable g ∧ ∀ (j : ℕ), Set.EqOn g (gLocal j) (disjointed (fun (k : ℕ) => interior (K k) ×ˢ J k) j)

Local L² gradient classes on a countable rectangle family admit a jointly measurable selection on the disjointed rectangle family.