Documentation

Dynamics.Drift

Drift theorems: from an expected potential drop to absorption #

Let Ψ ≥ 0 be a potential on a finite chain that vanishes exactly on the absorbed states, and that stays zero once it is zero. Two ways to turn its expected one-step behaviour into a bound on the absorption time, both from Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, Bounds on the voter model in dynamic networks, ICALP 2016, [arXiv:1603.01895]:

The _seq versions allow a time-dependent chain (iterateSeq) and time-dependent drift, as for the dynamic graphs of the paper; the others are their time-homogeneous specializations, stated with Kernel.event.

theorem Dynamics.Kernel.drift_absorption_seq {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (Ψ : α → ℝ) (c : ℕ → ℝ) (T : ℕ) (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hc : ∀ t < T, 0 ≤ c t) (hdrift : ∀ t < T, ∀ (x : α), 0 < Ψ x → (K t).apply Ψ x ≤ Ψ x - c t / Ψ x) (habs : ∀ t < T, ∀ (x : α), Ψ x = 0 → (K t).apply Ψ x = 0) (x₀ : α) (hT : 4 * Ψ x₀ ^ 2 ≤ ∑ t ∈ Finset.range T, c t) :
1 / 2 ≤ iterateSeq K T (fun (x : α) => if Ψ x = 0 then 1 else 0) x₀

Drift lemma, time-dependent form (Lemma 2.2 of Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, ICALP 2016). Let Ψ ≥ 0. Suppose that for every step t < T, the kernel K t lowers Ψ in expectation by at least c t / Ψ x from every state x with Ψ x > 0, and keeps Ψ at zero from every state with Ψ x = 0. If ∑_{t < T} c t ≥ 4 Ψ(x₀)², then started at x₀ the chain has Ψ = 0 (is absorbed) at time T with probability at least 1/2.

theorem Dynamics.Kernel.drift_absorption {α : Type u_1} [Fintype α] (K : Kernel α) (Ψ : α → ℝ) {c : ℝ} (hc : 0 ≤ c) (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hdrift : ∀ (x : α), 0 < Ψ x → K.apply Ψ x ≤ Ψ x - c / Ψ x) (habs : ∀ (x : α), Ψ x = 0 → K.apply Ψ x = 0) (x₀ : α) {T : ℕ} (hT : 4 * Ψ x₀ ^ 2 ≤ c * ↑T) :
1 / 2 ≤ K.event (fun (x : α) => Ψ x = 0) T x₀

Drift lemma (Lemma 2.2 of Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, ICALP 2016, for a single kernel). Let Ψ ≥ 0 satisfy 𝔼[Ψ_{t+1} | X_t = x] ≤ Ψ x - c / Ψ x whenever Ψ x > 0, and let the states with Ψ = 0 be absorbing for Ψ. Then the chain started at x₀ is absorbed by every time T with c T ≥ 4 Ψ(x₀)², with probability at least 1/2.

theorem Dynamics.Kernel.multiplicative_drift_seq {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (Ψ : α → ℝ) (δ : ℕ → ℝ) (T : ℕ) {Ψmin : ℝ} (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hmin : 0 < Ψmin) (hgap : ∀ (x : α), 0 < Ψ x → Ψmin ≤ Ψ x) (hdrift : ∀ t < T, ∀ (x : α), (K t).apply Ψ x ≤ (1 - δ t) * Ψ x) (x₀ : α) :
iterateSeq K T (fun (x : α) => if 0 < Ψ x then 1 else 0) x₀ ≤ (∏ t ∈ Finset.range T, (1 - δ t)) * Ψ x₀ / Ψmin

Multiplicative drift, time-dependent form (the argument of Lemma 2.4 of Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, ICALP 2016). Let Ψ ≥ 0, with every nonzero value at least Ψmin > 0. If for every step t < T the kernel K t satisfies 𝔼[Ψ_{t+1} | X_t = x] ≤ (1 - δ t) Ψ x from every state x (absorbed ones included), then the chain started at x₀ still has Ψ > 0 at time T with probability at most ∏_{t < T} (1 - δ t) Ψ(x₀) / Ψmin.

theorem Dynamics.Kernel.multiplicative_drift {α : Type u_1} [Fintype α] (K : Kernel α) (Ψ : α → ℝ) {δ Ψmin : ℝ} (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hmin : 0 < Ψmin) (hgap : ∀ (x : α), 0 < Ψ x → Ψmin ≤ Ψ x) (hdrift : ∀ (x : α), K.apply Ψ x ≤ (1 - δ) * Ψ x) (x₀ : α) (T : ℕ) :
K.event (fun (x : α) => 0 < Ψ x) T x₀ ≤ (1 - δ) ^ T * Ψ x₀ / Ψmin

Multiplicative drift (the argument of Lemma 2.4 of Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, ICALP 2016, for a single kernel). Let Ψ ≥ 0, with every nonzero value at least Ψmin > 0, and 𝔼[Ψ_{t+1} | X_t = x] ≤ (1 - δ) Ψ x from every state. Then the chain started at x₀ is not absorbed at time T with probability at most (1 - δ)^T Ψ(x₀) / Ψmin.