Covering a compact space-time set by ball cylinders inside a local box

The spatial factor Ω' of a local box is an arbitrary open set with compact closure, so no Sobolev extension is available on it and the embedding H¹ ↪ L⁶ cannot be applied there. The embedding is available on Euclidean balls, which is why CKN.ball_time_sobolev is stated on vec3Ball x₀ r.

This file supplies the geometry that bridges the two: a compact subset of the space-time carrier is covered by finitely many cylinders vec3Ball x_k r_k × J whose balls all lie inside the spatial factor of one local box. The time factor is never subdivided, because the interpolation on a ball accepts an arbitrary order-connected time interval; so the cover is indexed by one finite family and a finite union of integrability statements closes it.

Euclidean balls inside an open set

theorem CKN.vec3Ball_subset_ball (x : Foundation.Parabolic.Vec3) (r : ℝ) : Foundation.Parabolic.vec3Ball x r ⊆ Metric.ball x r

A Euclidean ball of Vec3 is contained in the metric ball of the same centre and radius for the ambient supremum norm.

theorem CKN.mem_vec3Ball_self {x : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : x ∈ Foundation.Parabolic.vec3Ball x r

The centre of a Euclidean ball of positive radius belongs to it.

theorem CKN.exists_vec3Ball_subset_of_isOpen {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {x : Foundation.Parabolic.Vec3} (hx : x ∈ U) : ∃ (r : ℝ), 0 < r ∧ Foundation.Parabolic.vec3Ball x r ⊆ U

Every point of an open subset of Vec3 has a Euclidean ball around it inside the set.

The finite cover

theorem CKN.exists_localBox_ball_cover_of_compact_subset {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hIord : I.OrdConnected) {K : Set Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) : ∃ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (n : ℕ) (c : Fin n → Foundation.Parabolic.Vec3) (r : Fin n → ℝ), localBox Ω I Ω' J ∧ (∀ (m : Fin n), 0 < r m) ∧ (∀ (m : Fin n), Foundation.Parabolic.vec3Ball (c m) (r m) ⊆ Ω') ∧ K ⊆ ⋃ (m : Fin n), spaceTimeSet (Foundation.Parabolic.vec3Ball (c m) (r m)) J

A compact subset of the space-time carrier sits inside a local box whose spatial factor is covered, over that same compact set, by finitely many Euclidean balls of the factor. The time factor of the box is used unchanged for every ball.

theorem CKN.exists_localBox_ball_cover_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) {K : Set Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) : ∃ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (n : ℕ) (c : Fin n → Foundation.Parabolic.Vec3) (r : Fin n → ℝ), localBox Ω I Ω' J ∧ (∀ (m : Fin n), 0 < r m) ∧ (∀ (m : Fin n), Foundation.Parabolic.vec3Ball (c m) (r m) ⊆ Ω') ∧ K ⊆ ⋃ (m : Fin n), spaceTimeSet (Foundation.Parabolic.vec3Ball (c m) (r m)) J

The ball cover of the previous statement, phrased for the data clauses of def:sws, which supply the openness and order-connectedness hypotheses.