A fixed finite cover of the unit spatial ball

A single finite cover, transported by translation and dilation, supplies the spatial covers used to move the Gaussian center.

theorem ESS.uc_unit_ball_finite_half_cover : ∃ (F : Finset CKN.Foundation.Parabolic.Vec3), (∀ c ∈ F, c ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 1)) ∧ ∀ y ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 1), ∃ c ∈ F, y ∈ CKN.Foundation.Parabolic.vec3Ball c (1 / 2)

The closed unit ball admits a finite cover by explicit Euclidean balls of radius one half, with centers in the closed unit ball.

theorem ESS.uc_finite_half_cover_scaled (F : Finset CKN.Foundation.Parabolic.Vec3) (hF : ∀ y ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 1), ∃ c ∈ F, y ∈ CKN.Foundation.Parabolic.vec3Ball c (1 / 2)) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) (y : CKN.Foundation.Parabolic.Vec3) (hy : y ∈ closure (CKN.Foundation.Parabolic.vec3Ball x r)) : ∃ c ∈ F, y ∈ CKN.Foundation.Parabolic.vec3Ball (x + r • c) (r / 2)

A fixed unit-ball cover scales to every positive spatial radius.

def ESS.ucBallCoverCenters (F : Finset CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : ℕ → Finset CKN.Foundation.Parabolic.Vec3

Centers obtained by repeatedly halving a spatial-ball cover.

Equations

• One or more equations did not get rendered due to their size.
• ESS.ucBallCoverCenters F x r 0 = {x}

theorem ESS.uc_ball_cover_centers_cover (F : Finset CKN.Foundation.Parabolic.Vec3) (hF : ∀ y ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 1), ∃ c ∈ F, y ∈ CKN.Foundation.Parabolic.vec3Ball c (1 / 2)) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3) : y ∈ CKN.Foundation.Parabolic.vec3Ball x r → ∃ c ∈ ucBallCoverCenters F x r n, y ∈ CKN.Foundation.Parabolic.vec3Ball c (r / 2 ^ n)

Every ball is covered by the iterated half-radius balls.

theorem ESS.uc_ball_cover_centers_card_le (F : Finset CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (n : ℕ) : (ucBallCoverCenters F x r n).card ≤ F.card ^ n

The number of iterated cover centers grows at most geometrically.

theorem ESS.uc_ball_cover_near_centers (F : Finset CKN.Foundation.Parabolic.Vec3) (hF : ∀ y ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 1), ∃ c ∈ F, y ∈ CKN.Foundation.Parabolic.vec3Ball c (1 / 2)) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) (n : ℕ) : ∃ (G : Finset CKN.Foundation.Parabolic.Vec3), G.card ≤ F.card ^ n ∧ (∀ c ∈ G, c ∈ CKN.Foundation.Parabolic.vec3Ball x (2 * r)) ∧ ∀ y ∈ CKN.Foundation.Parabolic.vec3Ball x r, ∃ c ∈ G, y ∈ CKN.Foundation.Parabolic.vec3Ball c (r / 2 ^ n)

Retain only cover balls meeting the original ball. Their centers stay within twice its radius.