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)

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

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

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

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) ≤ ε

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) ≤ ε₁ + ε₂

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

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

noncomputable def chainingSequenceReverse {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hxA : x ∈ C k) : ℕ → E

Equations

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

@[simp]

theorem chainingSequenceReverse_zero {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hxA : x ∈ C k) : chainingSequenceReverse hC hxA 0 = x

theorem chainingSequenceReverse_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) (hxA : x ∈ C k) (n : ℕ) : chainingSequenceReverse hC hxA (n + 1) = nearestPt (C (k - (n + 1))) (chainingSequenceReverse hC hxA n)

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 hC hxA n ∈ C (k - n)

noncomputable def chainingSequence {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hxA : x ∈ C k) (n : ℕ) : E

Equations

• chainingSequence hC hxA n = if n ≤ k then chainingSequenceReverse hC hxA (k - n) else x

theorem chainingSequence_of_eq {E : Type u_1} {x : E} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (hxA : x ∈ C k) : chainingSequence hC hxA k = x

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 hC hxA n ∈ C n

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) (hxA : x ∈ C k) (n : ℕ) (hn : n < k) : edist (chainingSequence hC hxA (n + 1)) (chainingSequence hC hxA n) ≤ ε n

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) (hxA : x ∈ C k) (m : ℕ) (hm : m ≤ k) : edist (chainingSequence hC hxA m) x ≤ ∑ i ∈ Finset.range (k - m), ε (m + i)

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) (hxA : x ∈ C k) (hyA : y ∈ C n) (m : ℕ) (hm : m ≤ k) (hn : m ≤ n) : edist (chainingSequence hC hxA m) (chainingSequence hC hyA m) ≤ edist x y + ∑ i ∈ Finset.range (k - m), ε (m + i) + ∑ j ∈ Finset.range (n - m), ε (m + j)

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) (hxA : x ∈ C k) (hyA : y ∈ C n) (m : ℕ) (hm : m ≤ k) (hn : m ≤ n) : edist (chainingSequence hC hxA m) (chainingSequence hC hyA m) ≤ edist x y + ε₀ * 4 * 2⁻¹ ^ m

theorem scale_change {E : Type u_1} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} {F : Type u_2} [PseudoEMetricSpace F] (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (m : ℕ) (hm : m ≤ k) (X : E → F) (δ : ENNReal) : ⨆ (s : E), ⨆ (t : E), ⨆ (_ : s ∈ C k), ⨆ (_ : t ∈ C k), ⨆ (_ : edist s t ≤ δ), edist (X s) (X t) ≤ ⨆ (s : E), ⨆ (t : E), ⨆ (hs : s ∈ C k), ⨆ (ht : t ∈ C k), ⨆ (_ : edist s t ≤ δ), edist (X (chainingSequence hC hs m)) (X (chainingSequence hC ht m)) + 2 * ⨆ (s : E), ⨆ (hs : s ∈ C k), edist (X s) (X (chainingSequence hC hs m))

theorem scale_change_rpow {E : Type u_1} {A : Set E} [PseudoEMetricSpace E] {ε : ℕ → ENNReal} {C : ℕ → Finset E} {k : ℕ} {F : Type u_2} [PseudoEMetricSpace F] (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A) (m : ℕ) (hm : m ≤ k) (X : E → F) (δ : ENNReal) (p : NNReal) : ⨆ (s : E), ⨆ (t : E), ⨆ (_ : s ∈ C k), ⨆ (_ : t ∈ C k), ⨆ (_ : edist s t ≤ δ), edist (X s) (X t) ^ ↑p ≤ 2 ^ ↑p * ⨆ (s : E), ⨆ (t : E), ⨆ (hs : s ∈ C k), ⨆ (ht : t ∈ C k), ⨆ (_ : edist s t ≤ δ), edist (X (chainingSequence hC hs m)) (X (chainingSequence hC ht m)) ^ ↑p + 4 ^ ↑p * ⨆ (s : E), ⨆ (hs : s ∈ C k), edist (X s) (X (chainingSequence hC hs m)) ^ ↑p