Compactness Cover

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_uniform_euclidean_ball_subset_open {K W : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) : ∃ (δ : ℝ), 0 < δ ∧ ∀ x ∈ K, euclideanBall x δ ⊆ W

Balls of one Euclidean radius about a compact set remain in an open neighborhood of that set.

theorem CKN.Leray.exists_uniform_finite_euclidean_ball_cover_with_bounded_overlap {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) : ∃ (N : ℕ), ∀ (r : ℝ), 0 < r → ∃ (s : Fin N → Set { x : Foundation.Parabolic.Vec3 // x ∈ K }), (∀ (i : Fin N), (s i).PairwiseDisjoint fun (x : { x : Foundation.Parabolic.Vec3 // x ∈ K }) => Metric.closedBall (Foundation.Parabolic.vec3Homeomorph ↑x) r) ∧ ∃ (t : Finset ((i : Fin N) × { x : { x : Foundation.Parabolic.Vec3 // x ∈ K } // x ∈ s i })), K ⊆ ⋃ p ∈ t, Foundation.Parabolic.vec3Ball (↑↑p.snd) r

One overlap-color count works for every radius in covers of a fixed compact set.

theorem CKN.Leray.exists_weighted_colored_finite_vec3_ball_cover {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) : ∃ (N : ℕ), ∀ (r : ℝ), 0 < r → ∃ (s : Fin N → Set { x : Foundation.Parabolic.Vec3 // x ∈ K }) (t : Finset ((i : Fin N) × { x : { x : Foundation.Parabolic.Vec3 // x ∈ K } // x ∈ s i })) (φ : ↥t → Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin N), (s i).PairwiseDisjoint fun (x : { x : Foundation.Parabolic.Vec3 // x ∈ K }) => Metric.closedBall (Foundation.Parabolic.vec3Homeomorph ↑x) r) ∧ K ⊆ ⋃ p ∈ t, Foundation.Parabolic.vec3Ball (↑↑p.snd) r ∧ (∀ (p : ↥t), Measurable (φ p)) ∧ (∀ (p : ↥t) (y : Foundation.Parabolic.Vec3), 0 ≤ φ p y ∧ φ p y ≤ 1) ∧ (∀ y ∈ K, ∑ p : ↥t, φ p y = 1) ∧ (∀ (p : ↥t), ∀ y ∈ K, φ p y ≠ 0 → y ∈ Foundation.Parabolic.vec3Ball (↑↑(↑p).snd) r) ∧ (∀ (p : ↥t), ∀ y ∉ K, φ p y = 0) ∧ ∀ (p q : ↥t), p ≠ q → (↑p).fst = (↑q).fst → Disjoint (Foundation.Parabolic.vec3Ball (↑↑(↑p).snd) r) (Foundation.Parabolic.vec3Ball (↑↑(↑q).snd) r)

A compact region has a finite equal-radius ball cover with a measurable partition of unity and finitely many disjoint colors.