A hitting-time bound for chains with multiplicative growth

Claim 2.9 of Doerr, Goldberg, Minder, Sauerwald, Scheideler, Stabilizing consensus with the power of two choices, SPAA 2011 (its proof is omitted there). It is the symmetry-breaking step of the binary median (2-Choices) dynamics from an almost balanced configuration, see Becchetti, Clementi, Natale, Consensus dynamics: an overview, SIGACT News 2020, §4 Case 3, where it is applied to X = ⌊s / (γ √n)⌋ (s the bias) with q = ⌊(n / 2) / (γ √n)⌋.

Let X be an observable of a finite chain with values in {0, …, q}. Suppose that from every state below the target, X grows by a factor c₁ > 1 (capped at q) in one step except with probability exp (-c₂ X), and that from every state with X = 0, X becomes positive with probability at least c₃ > 0. Then for every c₄, c₆ > 0 there is c₅ > 0, depending on c₁, c₂, c₃, c₄, c₆ only, such that X reaches c₄ log q within c₅ log q + log_{c₁} (c₄ log q) steps with probability at least 1 - q^{-c₆} (drift_hitting); equivalently within C log q steps (drift_hitting_log).

The chain is a Dynamics.Kernel on any finite state space and X is a function of the state. The source's Markov chain on {0, …, q} is the case X = Fin.val; the general form is the one needed by the application, where X is a function of the configuration. The target must be a value of X: c₄ log q ≤ q is assumed, since otherwise it is never hit.

theorem Dynamics.Kernel.drift_hitting {c₁ c₂ c₃ c₄ c₆ : ℝ} (hc₁ : 1 < c₁) (hc₂ : 0 < c₂) (hc₃ : 0 < c₃) (hc₄ : 0 < c₄) (hc₆ : 0 < c₆) : ∃ (c₅ : ℝ), 0 < c₅ ∧ ∀ {α : Type u} [inst : Fintype α] (K : Kernel α) (X : α → ℕ) (q : ℕ), (∀ (a : α), X a ≤ q) → (∀ (a : α), ↑(X a) < c₄ * Real.log ↑q → 1 - Real.exp (-(c₂ * ↑(X a))) ≤ (K a).prob fun (b : α) => min (c₁ * ↑(X a)) ↑q ≤ ↑(X b)) → (∀ (a : α), X a = 0 → c₃ ≤ (K a).prob fun (b : α) => 1 ≤ X b) → c₄ * Real.log ↑q ≤ ↑q → ∀ (a₀ : α) (t : ℕ), c₅ * Real.log ↑q + Real.logb c₁ (c₄ * Real.log ↑q) ≤ ↑t → 1 - ↑q ^ (-c₆) ≤ K.hitProb (fun (b : α) => c₄ * Real.log ↑q ≤ ↑(X b)) t a₀

Hitting-time bound (Claim 2.9 of Doerr, Goldberg, Minder, Sauerwald, Scheideler, SPAA 2011). Let c₁ > 1 and c₂, c₃, c₄, c₆ > 0. There is c₅ > 0 such that the following holds for every finite chain K and observable X with values in {0, …, q} such that the target c₄ log q is at most q. Suppose that from every state a below the target, the next state b has X b ≥ min (c₁ X a) q with probability at least 1 - exp (-c₂ X a), and that from every state with X a = 0, the next state has X b ≥ 1 with probability at least c₃. Then from any start a₀, the hitting time T = min {t : X_t ≥ c₄ log q} satisfies T ≤ t with probability at least 1 - q^{-c₆}, for every t ≥ c₅ log q + log_{c₁} (c₄ log q).

theorem Dynamics.Kernel.drift_hitting_log {c₁ c₂ c₃ c₄ c₆ : ℝ} (hc₁ : 1 < c₁) (hc₂ : 0 < c₂) (hc₃ : 0 < c₃) (hc₄ : 0 < c₄) (hc₆ : 0 < c₆) : ∃ (C : ℝ), 0 < C ∧ ∀ {α : Type u} [inst : Fintype α] (K : Kernel α) (X : α → ℕ) (q : ℕ), (∀ (a : α), X a ≤ q) → (∀ (a : α), ↑(X a) < c₄ * Real.log ↑q → 1 - Real.exp (-(c₂ * ↑(X a))) ≤ (K a).prob fun (b : α) => min (c₁ * ↑(X a)) ↑q ≤ ↑(X b)) → (∀ (a : α), X a = 0 → c₃ ≤ (K a).prob fun (b : α) => 1 ≤ X b) → c₄ * Real.log ↑q ≤ ↑q → ∀ (a₀ : α) (t : ℕ), C * Real.log ↑q ≤ ↑t → 1 - ↑q ^ (-c₆) ≤ K.hitProb (fun (b : α) => c₄ * Real.log ↑q ≤ ↑(X b)) t a₀

Hitting-time bound, O(log q) form (Claim 2.9 of Doerr, Goldberg, Minder, Sauerwald, Scheideler, SPAA 2011, with the term log_{c₁} (c₄ log q) absorbed into the constant). Under the hypotheses of drift_hitting, there is C > 0, depending on c₁, c₂, c₃, c₄, c₆ only, such that X reaches c₄ log q within any t ≥ C log q steps with probability at least 1 - q^{-c₆}.