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}
[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
@[simp]
theorem
chainingSequenceReverse_zero
{E : Type u_1}
{x : E}
[PseudoEMetricSpace E]
{C : ℕ → Finset E}
{k : ℕ}
:
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)
theorem
chainingSequenceReverse_of_pos
{E : Type u_1}
{x : E}
[PseudoEMetricSpace E]
{C : ℕ → Finset E}
{k n : ℕ}
(hn : 0 < n)
:
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
@[simp]
theorem
chainingSequence_of_eq
{E : Type u_1}
{x : E}
[PseudoEMetricSpace E]
{C : ℕ → Finset E}
{k : ℕ}
:
theorem
chainingSequence_of_lt
{E : Type u_1}
{x : E}
[PseudoEMetricSpace E]
{C : ℕ → Finset E}
{k n : ℕ}
(hkn : n < k)
:
theorem
chainingSequence_chainingSequence
{E : Type u_1}
{x : E}
[PseudoEMetricSpace E]
{C : ℕ → Finset E}
{k : ℕ}
(n : ℕ)
(hn : n ≤ k)
(m : ℕ)
(hm : m ≤ n)
:
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)))
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)))
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)
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 : { 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 C (↑s) k m)) (X (chainingSequence C (↑↑t) k m))) + 2 * ⨆ (s : { x : E // x ∈ C k }), edist (X ↑s) (X (chainingSequence C (↑s) k m))
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 : { 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 C (↑s) k m)) (X (chainingSequence C (↑↑t) k m)) ^ p) + 4 ^ p * ⨆ (s : { x : E // x ∈ C k }), edist (X ↑s) (X (chainingSequence C (↑s) k m)) ^ p