Chaining

References

• https://arxiv.org/pdf/2107.13837.pdf Lemma 6.2
• Talagrand, The generic chaining
• Vershynin, High-Dimensional Probability (section 4.2 and chapter 8)

def π {E : Type u_1} [Dist E] (s : Finset E) (x : E) : E

Closest point to x in the finite set s.

Equations

• π s x = sorry

theorem π_mem {E : Type u_1} {x : E} [Dist E] {s : Finset E} : π s x ∈ s

theorem dist_π_le {E : Type u_1} {x y : E} [Dist E] {s : Finset E} (hy : y ∈ s) : dist x (π s x) ≤ dist x y

noncomputable def πCov {E : Type u_1} [Dist E] (A : Set E) (ε : ℝ) (x : E) : E

Closest point to x in a minimal ε-cover of A.

Equations

• πCov A ε x = π (minimalCover ε A) x

theorem dist_πCov {E : Type u_1} {x : E} {A : Set E} [Dist E] {ε : ℝ} (hxA : x ∈ A) : dist x (πCov A ε x) ≤ ε

theorem dist_πCov_πCov_le_add {E : Type u_1} {x : E} {A : Set E} [PseudoMetricSpace E] {ε₁ ε₂ : ℝ} (hxA : x ∈ A) : dist (πCov A ε₁ x) (πCov A ε₂ x) ≤ ε₁ + ε₂

theorem dist_πCov_succ_le_two_mul {E : Type u_1} {x : E} {A : Set E} [PseudoMetricSpace E] {ε : ℕ → ℝ} (hε : Antitone ε) {i : ℕ} (hxA : x ∈ A) : dist (πCov A (ε i) x) (πCov A (ε (i + 1)) x) ≤ 2 * ε i

theorem dist_πCov_le_add_dist {E : Type u_1} {x y : E} {A : Set E} [PseudoMetricSpace E] {ε : ℝ} (hxA : x ∈ A) (hyA : y ∈ A) : dist (πCov A ε x) (πCov A ε y) ≤ 2 * ε + dist x y