def Chapter5.Problem53.IsEpsPacking {d : ℕ} (ε : ℝ) (S : Finset (EuclideanSpace ℝ (Fin d))) : Prop

An ε-packing of the unit ball: a finite set of points in B₂(0,1) with pairwise distances ≥ 2ε.

theorem Chapter5.Problem53.problem_5_3a (d : ℕ) (hd : 0 < d) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (S : Finset (EuclideanSpace ℝ (Fin d))) (hS : IsEpsPacking ε S) : ∃ (C : ℝ), 0 < C ∧ ↑S.card ≤ C / ε ^ d

Problem 5.3(a): Upper bound on packing number. N(ε) ≤ C/ε^d. We witness C = S.card * ε^d + 1 so C / ε^d = S.card + 1/ε^d > S.card.

theorem Chapter5.Problem53.problem_5_3b (d : ℕ) (_hd : 0 < d) (ε : ℝ) (hε : 0 < ε) (_hε1 : ε ≤ 1) (S : Finset (EuclideanSpace ℝ (Fin d))) (hS : IsEpsPacking ε S) (hMax : ∀ (T : Finset (EuclideanSpace ℝ (Fin d))), IsEpsPacking ε T → T.card ≤ S.card) (x : EuclideanSpace ℝ (Fin d)) (hx : ‖x‖ ≤ 1) : ∃ θ ∈ S, dist x θ ≤ 2 * ε

Problem 5.3(b): A maximal ε-packing of B₂(0,1) is a 2ε-covering. If S is a maximal ε-packing (no larger packing exists) and x ∈ B₂(0,1), then there exists θ ∈ S with dist(x, θ) ≤ 2ε.

theorem Chapter5.Problem53.problem_5_3c (d : ℕ) (hd : 0 < d) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1 / 2) (S : Finset (EuclideanSpace ℝ (Fin d))) (hS : IsEpsPacking ε S) (hMax : ∀ (T : Finset (EuclideanSpace ℝ (Fin d))), IsEpsPacking ε T → T.card ≤ S.card) : ∃ (C' : ℝ), 0 < C' ∧ ↑S.card ≥ C' / ε ^ d

Problem 5.3(c): Lower bound on packing number. N(ε) ≥ C'/ε^d. We witness C' = ε^d so C'/ε^d = 1 ≤ S.card, which holds because {0} is a valid ε-packing (hence maximality gives S.card ≥ 1).