Chaining

Given finite sets C n that cover a set A at scales ε n, chaining approximates a point x ∈ C k successively by points of C (k - 1), C (k - 2), ..., C 0. Bounds on the increments of a process along these chains give bounds on its suprema over A.

Main definitions

• Finset.nearestPt s x: a point of the finite set s that is closest to x.
• chainingSeq C x k n: the approximation of x at level n. It is x for k ≤ n, and the nearest point in C n of the approximation at level n + 1 for n < k.

Main statements

• edist_chainingSeq_le_sum: if each C i is an ε i-cover of A contained in A and x ∈ C k, the distance between x and its approximation at level m ≤ k is at most ∑ i ∈ Finset.range (k - m), ε (m + i).
• edist_chainingSeq_pow_two_le: for the scales ε₀ * 2⁻¹ ^ i, the approximations at level m of x ∈ C k and y ∈ C n are at distance at most edist x y + ε₀ * 4 * 2⁻¹ ^ m.
• iSup_edist_le_iSup_edist_chainingSeq: the supremum of edist (X s) (X t) over the pairs of points of C k at distance at most δ is bounded by the same supremum for their approximations at level m, plus twice the supremum of edist (X s) (X (chainingSeq C s k m)).

References

• [R. Vershynin, High-dimensional probability, Chapter 8][vershynin2018high]
• [M. Talagrand, Upper and lower bounds for stochastic processes][talagrand2014]

noncomputable def Finset.nearestPt {E : Type u_1} [EDist E] (s : Finset E) (x : E) : E

A point of the finite set s that is closest to x, or x if s is empty.

Equations

• s.nearestPt x = if hs : s.Nonempty then ⋯.choose else x

theorem Finset.nearestPt_mem {E : Type u_1} [EDist E] {s : Finset E} {x : E} (hs : s.Nonempty) : s.nearestPt x ∈ s

theorem Finset.edist_nearestPt_le {E : Type u_1} [EDist E] {s : Finset E} {x y : E} (hy : y ∈ s) : edist x (s.nearestPt x) ≤ edist x y

theorem Metric.IsCover.edist_nearestPt_le {E : Type u_1} [PseudoEMetricSpace E] {x : E} {A : Set E} {C : Finset E} {ε : NNReal} (hC : IsCover ε A ↑C) (hxA : x ∈ A) : edist x (C.nearestPt x) ≤ ↑ε

If C is an ε-cover of A, the nearest point in C of a point of A is at distance at most ε.

theorem edist_nearestPt_nearestPt_le_add {E : Type u_1} [PseudoEMetricSpace E] {x : E} {A : Set E} {C₁ C₂ : Finset E} {ε₁ ε₂ : NNReal} (hC₁ : Metric.IsCover ε₁ A ↑C₁) (hC₂ : Metric.IsCover ε₂ A ↑C₂) (hxA : x ∈ A) : edist (C₁.nearestPt x) (C₂.nearestPt x) ≤ ↑ε₁ + ↑ε₂

theorem edist_nearestPt_succ_le_two_mul {E : Type u_1} [PseudoEMetricSpace E] {x : E} {A : Set E} {ε : ℕ → NNReal} {C : ℕ → Finset E} (hC : ∀ (i : ℕ), Metric.IsCover (ε i) A ↑(C i)) (hε : Antitone ε) {i : ℕ} (hxA : x ∈ A) : edist ((C i).nearestPt x) ((C (i + 1)).nearestPt x) ≤ 2 * ↑(ε i)

theorem edist_nearestPt_le_add_dist {E : Type u_1} [PseudoEMetricSpace E] {x y : E} {A : Set E} {C : Finset E} {ε : NNReal} (hC : Metric.IsCover ε A ↑C) (hxA : x ∈ A) (hyA : y ∈ A) : edist (C.nearestPt x) (C.nearestPt y) ≤ 2 * ↑ε + edist x y

@[irreducible]

noncomputable def chainingSeq {E : Type u_1} [EDist E] (C : ℕ → Finset E) (x : E) (k n : ℕ) : E

The chaining sequence of x at level k: its term at level n is x if k ≤ n, and the nearest point in C n of the term at level n + 1 if n < k.

Equations

• chainingSeq C x k n = if h : n < k then (C n).nearestPt (chainingSeq C x k (n + 1)) else x

theorem chainingSeq_of_lt {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k n : ℕ} (hnk : n < k) : chainingSeq C x k n = (C n).nearestPt (chainingSeq C x k (n + 1))

theorem chainingSeq_of_le {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k n : ℕ} (hkn : k ≤ n) : chainingSeq C x k n = x

@[simp]

theorem chainingSeq_self {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k : ℕ} : chainingSeq C x k k = x

theorem chainingSeq_mem {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k n : ℕ} (hC : ∀ (i : ℕ), (C i).Nonempty) (hxC : x ∈ C k) (hn : n ≤ k) : chainingSeq C x k n ∈ C n

If the sets C i are nonempty and x ∈ C k, the term at level n ≤ k of the chaining sequence of x belongs to C n.

theorem chainingSeq_chainingSeq {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k : ℕ} (n : ℕ) (hn : n ≤ k) (m : ℕ) (hm : m ≤ n) : chainingSeq C (chainingSeq C x k n) n m = chainingSeq C x k m

The chaining sequence at level n of the term at level n of the chaining sequence of x at level k agrees with the latter below n.

theorem edist_chainingSeq_le_sum_edist {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k : ℕ} {T : Type u_2} [PseudoEMetricSpace T] (f : E → T) {m : ℕ} (hm : m ≤ k) : edist (f x) (f (chainingSeq C x k m)) ≤ ∑ i ∈ Finset.range (k - m), edist (f (chainingSeq C x k (m + i))) (f (chainingSeq C x k (m + i + 1)))

The distance between the images of x and of its approximation at level m is at most the sum of the distances between the images of consecutive terms of the chaining sequence.

theorem edist_chainingSeq_le_sum_edist' {E : Type u_1} [EDist E] {x : E} {C : ℕ → Finset E} {k : ℕ} {T : Type u_2} [PseudoEMetricSpace T] (f : E → T) {m : ℕ} (hm : m ≤ k) : edist (f (chainingSeq C x k m)) (f x) ≤ ∑ i ∈ Finset.range (k - m), edist (f (chainingSeq C x k (m + i + 1))) (f (chainingSeq C x k (m + i)))

theorem edist_chainingSeq_add_one {E : Type u_1} [PseudoEMetricSpace E] {x : E} {A : Set E} {ε : ℕ → NNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), Metric.IsCover (ε i) A ↑(C i)) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (n : ℕ) (hn : n < k) : edist (chainingSeq C x k (n + 1)) (chainingSeq C x k n) ≤ ↑(ε n)

Two consecutive terms of the chaining sequence of x ∈ C k are at distance at most ε n at level n < k.

theorem edist_chainingSeq_add_one_self {E : Type u_1} [PseudoEMetricSpace E] {x : E} {A : Set E} {ε : ℕ → NNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), Metric.IsCover (ε i) A ↑(C i)) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C (k + 1)) : edist (chainingSeq C x (k + 1) k) x ≤ ↑(ε k)

theorem edist_chainingSeq_le_sum {E : Type u_1} [PseudoEMetricSpace E] {x : E} {A : Set E} {ε : ℕ → NNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), Metric.IsCover (ε i) A ↑(C i)) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (m : ℕ) (hm : m ≤ k) : edist (chainingSeq C x k m) x ≤ ∑ i ∈ Finset.range (k - m), ↑(ε (m + i))

The approximation of x ∈ C k at level m ≤ k is at distance at most ∑ i ∈ Finset.range (k - m), ε (m + i) from x.

theorem edist_chainingSeq_le {E : Type u_1} [PseudoEMetricSpace E] {x y : E} {A : Set E} {ε : ℕ → NNReal} {C : ℕ → Finset E} {k n : ℕ} (hC : ∀ (i : ℕ), Metric.IsCover (ε i) A ↑(C i)) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (hyA : y ∈ C n) (m : ℕ) (hm : m ≤ k) (hn : m ≤ n) : edist (chainingSeq C x k m) (chainingSeq C y n m) ≤ edist x y + ∑ i ∈ Finset.range (k - m), ↑(ε (m + i)) + ∑ j ∈ Finset.range (n - m), ↑(ε (m + j))

Distance between the approximations at level m of x ∈ C k and y ∈ C n.

theorem edist_chainingSeq_pow_two_le {E : Type u_1} [PseudoEMetricSpace E] {x y : E} {A : Set E} {C : ℕ → Finset E} {k n : ℕ} {ε₀ : NNReal} (hC : ∀ (i : ℕ), Metric.IsCover (ε₀ * 2⁻¹ ^ i) A ↑(C i)) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (hyA : y ∈ C n) (m : ℕ) (hm : m ≤ k) (hn : m ≤ n) : edist (chainingSeq C x k m) (chainingSeq C y n m) ≤ edist x y + ↑ε₀ * 4 * 2⁻¹ ^ m

For the scales ε₀ * 2⁻¹ ^ i, the approximations at level m of x ∈ C k and y ∈ C n are at distance at most edist x y + ε₀ * 4 * 2⁻¹ ^ m.

theorem iSup_edist_le_iSup_edist_chainingSeq {E : Type u_1} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} {F : Type u_2} [PseudoEMetricSpace F] (m : ℕ) (X : E → F) (δ : ENNReal) : ⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ δ }), edist (X ↑s) (X ↑↑t) ≤ (⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ δ }), edist (X (chainingSeq C (↑s) k m)) (X (chainingSeq C (↑↑t) k m))) + 2 * ⨆ (s : ↥(C k)), edist (X ↑s) (X (chainingSeq C (↑s) k m))

The supremum of edist (X s) (X t) over the pairs of points of C k at distance at most δ is at most the same supremum for their approximations at level m, plus twice the supremum of edist (X s) (X (chainingSeq C s k m)).

theorem iSup_edist_rpow_le_iSup_edist_chainingSeq {E : Type u_1} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} {F : Type u_2} [PseudoEMetricSpace F] (m : ℕ) (X : E → F) (δ : ENNReal) (p : ℝ) (hp : 0 ≤ p) : ⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ δ }), edist (X ↑s) (X ↑↑t) ^ p ≤ (2 ^ p * ⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ δ }), edist (X (chainingSeq C (↑s) k m)) (X (chainingSeq C (↑↑t) k m)) ^ p) + 4 ^ p * ⨆ (s : ↥(C k)), edist (X ↑s) (X (chainingSeq C (↑s) k m)) ^ p

rpow version of iSup_edist_le_iSup_edist_chainingSeq.