Helpers for the hitting-time bound (Claim 2.9 of Doerr et al., SPAA 2011)

The proof of Dynamics.Kernel.drift_hitting (the paper omits it) applies the geometric drift bound one_sub_hitProb_le_of_drift to a potential V = g ∘ X off the target (V = 0 on it):

• g is antitone with values in (0, 1]. On the low levels x < x₀, where one step only guarantees X' ≥ x + 1 with probability p = min c₃ (1 - e^{-c₂}), it is g x = 1 - η (θ^x - 1) with θ = p⁻¹: this is the shape that makes p g(x + 1) + (1 - p) ≤ ρ g x hold with a single ρ < 1, however small p is. From the level x₀ on, where the growth X' ≥ c₁ x fails only with probability e^{-c₂ x}, it is g x = (1/2) e^{-(c₂/2)(x - x₀)} (exists_potential).
• One step of the chain decreases V by the factor ρ off the target (apply_potential_le), by the elementary bound expect_le_of_prob on a two-valued majorant.
• V ≤ 1 and V ≥ (1/2) e^{-(c₂/2) c₄ log q} = (1/2) q^{-c₂ c₄/2} off the target, so the non-hitting probability after t steps is at most 2 ρ^t q^{c₂ c₄/2}, which is below q^{-c₆} after O(log q) steps (two_mul_pow_mul_exp_le).

theorem Dynamics.Distribution.expect_le_of_prob {α : Type u_1} [Fintype α] (μ : Distribution α) {f : α → ℝ} {E : α → Prop} {m M s : ℝ} (hf : ∀ (b : α), f b ≤ M) (hE : ∀ (b : α), E b → f b ≤ m) (hmM : m ≤ M) (hs : s ≤ μ.prob E) : μ.expect f ≤ M - (M - m) * s

If f ≤ M everywhere and f ≤ m ≤ M on an event of probability at least s, then 𝔼 f ≤ M - (M - m) s.

theorem Dynamics.Kernel.exp_neg_le_quarter {u : ℝ} (hu : 3 ≤ u) : Real.exp (-u) ≤ 1 / 4

e^{-u} ≤ 1/4 for u ≥ 3 (from e^u ≥ 1 + u).

theorem Dynamics.Kernel.exists_threshold {θ β c₁ : ℝ} (hθ : 1 < θ) (hβ : 0 < β) (hc₁ : 1 < c₁) : ∃ (x₀ : ℕ), 1 ≤ x₀ ∧ 2 ≤ θ ^ x₀ ∧ Real.exp (-(β * (c₁ - 1) * ↑x₀)) ≤ 1 / 4 ∧ Real.exp (-(2 * β * ↑x₀)) ≤ 1 / 4

A threshold level x₀ ≥ 1 with θ^x₀ ≥ 2, e^{-β (c₁ - 1) x₀} ≤ 1/4 and e^{-2 β x₀} ≤ 1/4.

theorem Dynamics.Kernel.low_drift_ineq {p η θ T : ℝ} (hp1 : p < 1) (hη : 0 ≤ η) (hpθ : p * θ = 1) (hT : 1 ≤ T) : p * (1 - η * (T * θ - 1)) + (1 - p) ≤ (1 - (1 - p) * η / 2) * (1 - η * (T - 1))

Low levels: with θ = p⁻¹, T = θ^x ≥ 1 and ρ = 1 - (1 - p) η / 2, the potential g x = 1 - η (θ^x - 1) satisfies p g(x + 1) + (1 - p) ≤ ρ g x. The slack is (1 - p) η (1 + η (T - 1)) / 2.

theorem Dynamics.Kernel.high_drift_ineq {β c₁ ρ x₀ x y : ℝ} (hβ : 0 ≤ β) (hc₁ : 1 ≤ c₁) (hρ : 3 / 4 ≤ ρ) (hx : x₀ ≤ x) (hy : c₁ * x ≤ y) (hq1 : Real.exp (-(β * (c₁ - 1) * x₀)) ≤ 1 / 4) (hq2 : Real.exp (-(2 * β * x₀)) ≤ 1 / 4) : 1 / 2 * Real.exp (-(β * (y - x₀))) + Real.exp (-(2 * β * x)) ≤ ρ * (1 / 2 * Real.exp (-(β * (x - x₀))))

High levels: for x₀ ≤ x and y ≥ c₁ x, the growth step lowers (1/2) e^{-β (· - x₀)} by e^{-β (c₁ - 1) x₀} ≤ 1/4, and the failure probability e^{-2 β x} is at most e^{-2 β x₀} ≤ 1/4 times e^{-β (x - x₀)}; so the expected potential is at most 3/8 e^{-β (x - x₀)} ≤ ρ g x once ρ ≥ 3/4.

theorem Dynamics.Kernel.exists_potential {c₁ c₂ p : ℝ} (hc₁ : 1 < c₁) (hc₂ : 0 < c₂) (hp : 0 < p) (hp1 : p < 1) : ∃ (ρ : ℝ), 0 < ρ ∧ ρ < 1 ∧ ∃ (g : ℕ → ℝ), Antitone g ∧ (∀ (x : ℕ), g x ≤ 1) ∧ (∀ (x : ℕ), 1 / 2 * Real.exp (-(c₂ / 2 * ↑x)) ≤ g x) ∧ ∀ (x : ℕ), p * g (x + 1) + (1 - p) ≤ ρ * g x ∨ 1 ≤ x ∧ ∀ (y : ℕ), c₁ * ↑x ≤ ↑y → g y + Real.exp (-(c₂ * ↑x)) ≤ ρ * g x

The potential. Let c₁ > 1, c₂ > 0, 0 < p < 1. There are ρ ∈ (0, 1) and an antitone g : ℕ → ℝ with (1/2) e^{-(c₂/2) x} ≤ g x ≤ 1, such that at every level x one of two drift inequalities holds: the low-level one p g(x + 1) + (1 - p) ≤ ρ g x (a step up by one with probability ≥ p, anything otherwise), or, for x ≥ 1, the high-level one g y + e^{-c₂ x} ≤ ρ g x for every y ≥ c₁ x (growth by c₁ except with probability e^{-c₂ x}).

theorem Dynamics.Kernel.apply_potential_le {α : Type u_1} [Fintype α] (K : Kernel α) (X : α → ℕ) (q : ℕ) {c₁ c₂ c₃ p ρ L : ℝ} {g : ℕ → ℝ} (hc₁ : 1 < c₁) (hc₂ : 0 ≤ c₂) (hpc₃ : p ≤ c₃) (hpc₂ : p ≤ 1 - Real.exp (-c₂)) (hρ : ρ ≤ 1) (hg : Antitone g) (hg0 : ∀ (x : ℕ), 0 ≤ g x) (hg1 : ∀ (x : ℕ), g x ≤ 1) (hdrift : ∀ (x : ℕ), p * g (x + 1) + (1 - p) ≤ ρ * g x ∨ 1 ≤ x ∧ ∀ (y : ℕ), c₁ * ↑x ≤ ↑y → g y + Real.exp (-(c₂ * ↑x)) ≤ ρ * g x) (hLq : L ≤ ↑q) (hgrow : ∀ (a : α), ↑(X a) < L → 1 - Real.exp (-(c₂ * ↑(X a))) ≤ (K a).prob fun (b : α) => min (c₁ * ↑(X a)) ↑q ≤ ↑(X b)) (hzero : ∀ (a : α), X a = 0 → c₃ ≤ (K a).prob fun (b : α) => 1 ≤ X b) {a : α} (ha : ↑(X a) < L) : K.apply (fun (b : α) => if L ≤ ↑(X b) then 0 else g (X b)) a ≤ ρ * g (X a)

One step of the potential. Let V = g ∘ X off the target L ≤ X and V = 0 on it, for a potential g as in exists_potential, and let the chain satisfy the hypotheses of Claim 2.9 below the target L ≤ q. Then 𝔼[V(X_{t+1}) | X_t = a] ≤ ρ g(X a) from every state a below the target. At a low level the step goes up by one with probability at least p ≤ min c₃ (1 - e^{-c₂}) (by the escape hypothesis at 0, by growth at X a ≥ 1); at a high level growth fails with probability at most e^{-c₂ X a}.

theorem Dynamics.Kernel.two_mul_pow_mul_exp_le {ρ b c ℓ D : ℝ} {t : ℕ} (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hℓ : Real.log 2 ≤ ℓ) (hD : 0 ≤ D) (ht : ((1 + b + c) / -Real.log ρ + D / Real.log 2) * ℓ - D ≤ ↑t) : 2 * ρ ^ t * Real.exp (b * ℓ) ≤ Real.exp (-(c * ℓ))

The final estimate. If ρ ∈ (0, 1), ℓ ≥ log 2, D ≥ 0 and t ≥ ((1 + b + c) / log (1/ρ) + D / log 2) ℓ - D, then 2 ρ^t e^{b ℓ} ≤ e^{-c ℓ}. With ℓ = log q this is 2 ρ^t q^b ≤ q^{-c}.