Consensus probability (Theorem 2.1)

Eventual consensus probability is the supremum of increasing finite-time probabilities. The proof bounds the discrepancy from invariant white mass by the probability of nonconsensus, then passes to the limit.

noncomputable def Voter.allColor {V : Type u_1} {C : Type u_2} [Fintype V] (c : C) (s : Config V C) : ℝ

Indicator of a specified consensus color.

Equations

• Voter.allColor c s = if s = fun (x : V) => c then 1 else 0

noncomputable def Voter.colorProbability {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (n : ℕ) (s : Config V C) : ℝ

Probability that all vertices have color c at time n.

Equations

• Voter.colorProbability H c n s = (Voter.transition H).iterate n (Voter.allColor c) s

noncomputable def Voter.eventualColor {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (s : Config V C) : ℝ

Eventual probability, defined from the finite-time consensus probabilities.

Equations

• Voter.eventualColor H c s = ⨆ (n : ℕ), Voter.colorProbability H c n s

theorem Voter.allColor_nonneg {V : Type u_1} {C : Type u_2} [Fintype V] (c : C) (s : Config V C) : 0 ≤ allColor c s

theorem Voter.allColor_le_one {V : Type u_1} {C : Type u_2} [Fintype V] (c : C) (s : Config V C) : allColor c s ≤ 1

theorem Voter.colorProbability_le_one {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (n : ℕ) (s : Config V C) : colorProbability H c n s ≤ 1

theorem Voter.colorProbability_mono {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (s : Config V C) : Monotone fun (n : ℕ) => colorProbability H c n s

theorem Voter.colorProbability_tendsto {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (s : Config V C) : Filter.Tendsto (fun (n : ℕ) => colorProbability H c n s) Filter.atTop (nhds (eventualColor H c s))

theorem Voter.colorProbability_constant {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (n : ℕ) : (colorProbability H c n fun (x : V) => c) = 1

A constant configuration retains its color at every finite time.

theorem Voter.eventualColor_constant {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) : (eventualColor H c fun (x : V) => c) = 1

A constant configuration reaches its own consensus color with probability one.

noncomputable def Voter.whiteMass {V : Type u_1} [Fintype V] (p : Dynamics.Distribution V) : Config V Bool → ℝ

Stationary white mass.

Equations

• Voter.whiteMass p = Voter.mass p fun (b : Bool) => if b = true then 1 else 0

theorem Voter.whiteMass_nonneg {V : Type u_1} [Fintype V] (p : Dynamics.Distribution V) (s : Config V Bool) : 0 ≤ whiteMass p s

theorem Voter.whiteMass_le_one {V : Type u_1} [Fintype V] (p : Dynamics.Distribution V) (s : Config V Bool) : whiteMass p s ≤ 1

theorem Voter.whiteMass_const {V : Type u_1} [Fintype V] (p : Dynamics.Distribution V) (c : Bool) : (whiteMass p fun (x : V) => c) = if c = true then 1 else 0

A constant configuration has white mass 1 if white, 0 if black.

theorem Voter.colorProbability_eq_event {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (c : C) (n : ℕ) (s : Config V C) : colorProbability H c n s = (transition H).event (fun (x : Config V C) => x = fun (x : V) => c) n s

Finite-time consensus on a color is an event.

theorem Voter.whiteMass_bounds {V : Type u_1} [Fintype V] [Nonempty V] (p : Dynamics.Distribution V) (s : Config V Bool) : allColor true s ≤ whiteMass p s ∧ whiteMass p s ≤ allColor true s + survival s

theorem Voter.whiteProbability_error {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (H : Dynamics.Kernel V) (p : Dynamics.Distribution V) (hp : H.Stationary p) (n : ℕ) (s : Config V Bool) : 0 ≤ whiteMass p s - colorProbability H true n s ∧ whiteMass p s - colorProbability H true n s ≤ (transition H).iterate n survival s

The finite-time discrepancy is at most nonconsensus probability (Lemma 2.2).

theorem Voter.whiteProbability_tendsto {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) (hc : G.Connected) (hn : ¬G.Colorable 2) (H : Dynamics.Kernel V) (hsupport : ∀ (i j : V), G.Adj i j → 0 < (H i).weight j) (p : Dynamics.Distribution V) (hp : H.Stationary p) (s : Config V Bool) : Filter.Tendsto (fun (n : ℕ) => colorProbability H true n s) Filter.atTop (nhds (whiteMass p s))

Finite-time all-white probability converges to initial stationary white mass.

theorem Voter.consensus_probability {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) (hc : G.Connected) (hn : ¬G.Colorable 2) (H : Dynamics.Kernel V) (hsupport : ∀ (i j : V), G.Adj i j → 0 < (H i).weight j) (p : Dynamics.Distribution V) (hp : H.Stationary p) (s : Config V Bool) : eventualColor H true s = whiteMass p s

Hassin–Peleg Theorem 2.1. Eventual all-white consensus probability is exactly the stationary weight of the initially white vertices.