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)
theorem
edist_nearestPt_le
{E : Type u_1}
{x y : E}
[PseudoEMetricSpace E]
{s : Finset E}
(hy : y ∈ s)
:
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)
Instances For
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)
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
Instances For
theorem
edist_chainingSequence_le_sum_edist
{E : Type u_1}
{x : E}
{A : Set E}
[PseudoEMetricSpace E]
{ε : ℕ → ENNReal}
{C : ℕ → Finset E}
{k : ℕ}
{T : Type u_2}
[PseudoEMetricSpace T]
(f : E → T)
{hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A}
{hxA : x ∈ C k}
{m : ℕ}
(hm : m ≤ k)
:
edist (f x) (f (chainingSequence hC hxA m)) ≤ ∑ i ∈ Finset.range (k - m), edist (f (chainingSequence hC hxA (m + i))) (f (chainingSequence hC hxA (m + i + 1)))
theorem
edist_chainingSequence_le_sum_edist'
{E : Type u_1}
{x : E}
{A : Set E}
[PseudoEMetricSpace E]
{ε : ℕ → ENNReal}
{C : ℕ → Finset E}
{k : ℕ}
{T : Type u_2}
[PseudoEMetricSpace T]
(f : E → T)
{hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) A}
{hxA : x ∈ C k}
{m : ℕ}
(hm : m ≤ k)
:
edist (f (chainingSequence hC hxA m)) (f x) ≤ ∑ i ∈ Finset.range (k - m), edist (f (chainingSequence hC hxA (m + i + 1))) (f (chainingSequence hC hxA (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)
(hCA : ∀ (i : ℕ), ↑(C 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
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 : ℕ)
(X : E → F)
(δ : ENNReal)
:
⨆ (s : { x : E // x ∈ C k }), ⨆ (t : { t : { x : E // x ∈ C k } // edist s t ≤ δ }), edist (X ↑s) (X ↑↑t) ≤ (⨆ (s : { x : E // x ∈ C k }),
⨆ (t : { t : { x : E // x ∈ C k } // edist s t ≤ δ }),
edist (X (chainingSequence hC ⋯ m)) (X (chainingSequence hC ⋯ m))) + 2 * ⨆ (s : { x : E // x ∈ C k }), edist (X ↑s) (X (chainingSequence hC ⋯ 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 : ℕ)
(X : E → F)
(δ : ENNReal)
(p : ℝ)
(hp : 0 ≤ p)
:
⨆ (s : { x : E // x ∈ C k }), ⨆ (t : { t : { x : E // x ∈ C k } // edist s t ≤ δ }), edist (X ↑s) (X ↑↑t) ^ p ≤ (2 ^ p * ⨆ (s : { x : E // x ∈ C k }),
⨆ (t : { t : { x : E // x ∈ C k } // edist s t ≤ δ }),
edist (X (chainingSequence hC ⋯ m)) (X (chainingSequence hC ⋯ m)) ^ p) + 4 ^ p * ⨆ (s : { x : E // x ∈ C k }), edist (X ↑s) (X (chainingSequence hC ⋯ m)) ^ p