# 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)

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

Closest point to `x` in the finite set `s`.

Equations

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

Instances For

source
theorem nearestPt_mem {E : Type u_1} {x : E} [EDist E] {s : Finset E} (hs : s.Nonempty) :
nearestPt s x ∈ s
source
theorem edist_nearestPt_le {E : Type u_1} {x y : E} [PseudoEMetricSpace E] {s : Finset E} (hy : y ∈ s) :
edist x (nearestPt s x) ≤ edist x y
source
theorem edist_nearestPt_of_isCover {E : Type u_1} {x : E} {A : Set E} {C : Finset E} {ε : ENNReal} [PseudoEMetricSpace E] (hC : IsCover (↑C) ε A) (hxA : x ∈ A) :
edist x (nearestPt C x) ≤ ε
source
theorem edist_nearestPt_nearestPt_le_add {E : Type u_1} {x : E} {A : Set E} {C₁ C₂ : Finset E} {ε₁ ε₂ : ENNReal} [PseudoEMetricSpace E] (hC₁ : IsCover (↑C₁) ε₁ A) (hC₂ : IsCover (↑C₂) ε₂ A) (hxA : x ∈ A) :
edist (nearestPt C₁ x) (nearestPt C₂ x) ≤ ε₁ + ε₂
source
theorem edist_nearestPt_succ_le_two_mul {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hε : Antitone ε) {i : ℕ} (hxA : x ∈ A) :
edist (nearestPt (C i) x) (nearestPt (C (i + 1)) x) ≤ 2 * ε i
source
theorem edist_nearestPt_le_add_dist {E : Type u_1} {x y : E} {A : Set E} {C : Finset E} {ε : ENNReal} [PseudoEMetricSpace E] (hC : IsCover (↑C) ε A) (hxA : x ∈ A) (hyA : y ∈ A) :
edist (nearestPt C x) (nearestPt C y) ≤ 2 * ε + edist x y
source
noncomputable def chainingSequenceReverse {E : Type u_1} [PseudoEMetricSpace E] (C : ℕ → Finset E) (x : E) (k : ℕ) :
ℕ → E
Equations

- chainingSequenceReverse C x k 0 = x
- chainingSequenceReverse C x k n.succ = nearestPt (C (k - (n + 1))) (chainingSequenceReverse C x k n)

Instances For

source
@[simp]
theorem chainingSequenceReverse_zero {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} :
chainingSequenceReverse C x k 0 = x
source
theorem chainingSequenceReverse_add_one {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} (n : ℕ) :
chainingSequenceReverse C x k (n + 1) = nearestPt (C (k - (n + 1))) (chainingSequenceReverse C x k n)
source
theorem chainingSequenceReverse_of_pos {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k n : ℕ} (hn : 0 < n) :
chainingSequenceReverse C x k n = nearestPt (C (k - n)) (chainingSequenceReverse C x k (n - 1))
source
theorem chainingSequenceReverse_mem {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k n : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hA : A.Nonempty) (hxA : x ∈ C k) :
chainingSequenceReverse C x k n ∈ C (k - n)
source
noncomputable def chainingSequence {E : Type u_1} [PseudoEMetricSpace E] (C : ℕ → Finset E) (x : E) (k n : ℕ) :
E
Equations

- chainingSequence C x k n = if n ≤ k then chainingSequenceReverse C x k (k - n) else x

Instances For

source
@[simp]
theorem chainingSequence_of_eq {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} :
chainingSequence C x k k = x
source
theorem chainingSequence_of_lt {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k n : ℕ} (hkn : n < k) :
chainingSequence C x k n = nearestPt (C n) (chainingSequence C x k (n + 1))
source
theorem chainingSequence_mem {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hA : A.Nonempty) (hxA : x ∈ C k) (n : ℕ) (hn : n ≤ k) :
chainingSequence C x k n ∈ C n
source
theorem chainingSequence_chainingSequence {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} (n : ℕ) (hn : n ≤ k) (m : ℕ) (hm : m ≤ n) :
chainingSequence C (chainingSequence C x k n) n m = chainingSequence C x k m
source
theorem edist_chainingSequence_add_one {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (n : ℕ) (hn : n < k) :
edist (chainingSequence C x k (n + 1)) (chainingSequence C x k n) ≤ ε n
source
theorem edist_chainingSequence_add_one_self {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C (k + 1)) :
edist (chainingSequence C x (k + 1) k) x ≤ ε k
source
theorem edist_chainingSequence_le_sum_edist {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} {T : Type u_2} [PseudoEMetricSpace T] (f : E → T) {m : ℕ} (hm : m ≤ k) :
edist (f x) (f (chainingSequence C x k m)) ≤ ∑ i ∈ Finset.range (k - m), edist (f (chainingSequence C x k (m + i))) (f (chainingSequence C x k (m + i + 1)))
source
theorem edist_chainingSequence_le_sum_edist' {E : Type u_1} {x : E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k : ℕ} {T : Type u_2} [PseudoEMetricSpace T] (f : E → T) {m : ℕ} (hm : m ≤ k) :
edist (f (chainingSequence C x k m)) (f x) ≤ ∑ i ∈ Finset.range (k - m), edist (f (chainingSequence C x k (m + i + 1))) (f (chainingSequence C x k (m + i)))
source
theorem edist_chainingSequence_le_sum {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (m : ℕ) (hm : m ≤ k) :
edist (chainingSequence C x k m) x ≤ ∑ i ∈ Finset.range (k - m), ε (m + i)
source
theorem edist_chainingSequence_le {E : Type u_1} {x y : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k n : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (hyA : y ∈ C n) (m : ℕ) (hm : m ≤ k) (hn : m ≤ n) :
edist (chainingSequence C x k m) (chainingSequence C y n m) ≤ edist x y + ∑ i ∈ Finset.range (k - m), ε (m + i) + ∑ j ∈ Finset.range (n - m), ε (m + j)
source
theorem edist_chainingSequence_pow_two_le {E : Type u_1} {x y : E} {A : Set E} [PseudoEMetricSpace E] {C : ℕ → Finset E} {k n : ℕ} {ε₀ : ENNReal} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε₀ * 2⁻¹ ^ i) A) (hCA : ∀ (i : ℕ), ↑(C i) ⊆ A) (hxA : x ∈ C k) (hyA : y ∈ C n) (m : ℕ) (hm : m ≤ k) (hn : m ≤ n) :
edist (chainingSequence C x k m) (chainingSequence C y n m) ≤ edist x y + ε₀ * 4 * 2⁻¹ ^ m
source
theorem scale_change {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 (chainingSequence C (↑s) k m)) (X (chainingSequence C (↑↑t) k m))) + 2 * ⨆ (s : ↥(C k)), edist (X ↑s) (X (chainingSequence C (↑s) k m))
source
theorem scale_change_rpow {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 (chainingSequence C (↑s) k m)) (X (chainingSequence C (↑↑t) k m)) ^ p) + 4 ^ p * ⨆ (s : ↥(C k)), edist (X ↑s) (X (chainingSequence C (↑s) k m)) ^ p