Progress through nested phases

A finite Markov chain that, from every state of Aᵢ, stays in Aᵢ with probability ≥ 1 - ε and moves into the smaller set Aᵢ₊₁ with probability ≥ 1 - ν, reaches the innermost set A_T within ℓ T steps except with probability T (ℓ ε + ν^ℓ). This is Lemma A.4 of Becchetti, Clementi, Natale, Pasquale, Silvestri, Trevisan, Simple dynamics for plurality consensus (SPAA 2014); its proof is omitted there.

The proof works phase by phase with the survival observable outside B (the indicator of having left B): within ℓ steps the chain leaves Aᵢ with probability at most ℓ ε and fails to jump in each of the ℓ steps with probability at most ν^ℓ. The hypothesis ε ≤ ν of the paper is not needed.

noncomputable def Dynamics.Kernel.outside {α : Type u_1} (B : Set α) (b : α) : ℝ

Indicator of lying outside B.

Equations

• Dynamics.Kernel.outside B b = if b ∈ B then 0 else 1

theorem Dynamics.Kernel.outside_of_mem {α : Type u_1} {B : Set α} {b : α} (h : b ∈ B) : outside B b = 0

theorem Dynamics.Kernel.outside_of_not_mem {α : Type u_1} {B : Set α} {b : α} (h : b ∉ B) : outside B b = 1

theorem Dynamics.Kernel.outside_nonneg {α : Type u_1} (B : Set α) (b : α) : 0 ≤ outside B b

theorem Dynamics.Kernel.outside_le_one {α : Type u_1} (B : Set α) (b : α) : outside B b ≤ 1

theorem Dynamics.Kernel.iterate_le_one {α : Type u_1} [Fintype α] (K : Kernel α) (n : ℕ) {f : α → ℝ} (h : ∀ (a : α), f a ≤ 1) (a : α) : K.iterate n f a ≤ 1

theorem Dynamics.Kernel.apply_outside {α : Type u_1} [Fintype α] (K : Kernel α) (B : Set α) (a : α) : K.apply (outside B) a = 1 - (K a).prob fun (x : α) => x ∈ B

One step leaves B with probability 1 - P(stay in B).

theorem Dynamics.Kernel.event_eq_one_sub {α : Type u_1} [Fintype α] (K : Kernel α) (B : Set α) (n : ℕ) (a : α) : K.event (fun (x : α) => x ∈ B) n a = 1 - K.iterate n (outside B) a

Occupation probability is one minus the survival observable.

theorem Dynamics.Kernel.iterate_outside_le_of_stay {α : Type u_1} [Fintype α] (K : Kernel α) (B : Set α) {ε : ℝ} (hε : 0 ≤ ε) (hstay : ∀ a ∈ B, 1 - ε ≤ (K a).prob fun (x : α) => x ∈ B) (ℓ : ℕ) (a : α) : a ∈ B → K.iterate ℓ (outside B) a ≤ ↑ℓ * ε

Staying: if from every state of B the chain stays in B with probability ≥ 1 - ε, then it has left B after ℓ steps with probability at most ℓ ε.

theorem Dynamics.Kernel.iterate_outside_le_of_move {α : Type u_1} [Fintype α] (K : Kernel α) {A B : Set α} (hBA : B ⊆ A) {ε ν : ℝ} (hε : 0 ≤ ε) (hν : 0 ≤ ν) (hstayA : ∀ a ∈ A, 1 - ε ≤ (K a).prob fun (x : α) => x ∈ A) (hstayB : ∀ a ∈ B, 1 - ε ≤ (K a).prob fun (x : α) => x ∈ B) (hmove : ∀ a ∈ A, 1 - ν ≤ (K a).prob fun (x : α) => x ∈ B) (ℓ : ℕ) (a : α) : a ∈ A → K.iterate ℓ (outside B) a ≤ ↑ℓ * ε + ν ^ ℓ

One phase: from A, which is left with probability ≤ ε per step, the chain is outside B ⊆ A after ℓ steps with probability at most ℓ ε + ν^ℓ, if every step from A enters B with probability ≥ 1 - ν and B itself is left with probability ≤ ε per step.

theorem Dynamics.Kernel.nested_phases {α : Type u_1} [Fintype α] (K : Kernel α) (A : ℕ → Set α) {T : ℕ} (hT : 1 ≤ T) (ℓ : ℕ) {ε ν : ℝ} (hε : 0 ≤ ε) (hν : 0 ≤ ν) (hnest : ∀ (i : ℕ), 1 ≤ i → i < T → A (i + 1) ⊆ A i) (hstay : ∀ (i : ℕ), 1 ≤ i → i ≤ T → ∀ a ∈ A i, 1 - ε ≤ (K a).prob fun (x : α) => x ∈ A i) (hmove : ∀ (i : ℕ), 1 ≤ i → i < T → ∀ a ∈ A i, 1 - ν ≤ (K a).prob fun (x : α) => x ∈ A (i + 1)) (a : α) : a ∈ A 1 → 1 - ↑T * (↑ℓ * ε + ν ^ ℓ) ≤ K.event (fun (x : α) => x ∈ A T) (ℓ * T) a

Lemma A.4 (nested phases). Let A₁ ⊇ A₂ ⊇ ⋯ ⊇ A_T be such that from every state of Aᵢ the chain stays in Aᵢ with probability ≥ 1 - ε, and for i < T moves into Aᵢ₊₁ with probability ≥ 1 - ν. Then from any state of A₁, after ℓ T steps the chain lies in A_T with probability at least 1 - T (ℓ ε + ν^ℓ).