Almost-sure consensus from graph propagation

noncomputable def Voter.survival {V : Type u_1} [Fintype V] (s : Config V Bool) : ℝ

Indicator of nonconsensus.

Equations

• Voter.survival s = if ∃ (c : Bool), s = fun (x : V) => c then 0 else 1

theorem Voter.survival_binary {V : Type u_1} [Fintype V] (s : Config V Bool) : survival s = 0 ∨ survival s = 1

@[simp]

theorem Voter.survival_constant {V : Type u_1} [Fintype V] (c : Bool) : (survival fun (x : V) => c) = 0

theorem Voter.survival_eq {V : Type u_1} [Fintype V] (s : Config V Bool) : survival s = if (¬s = fun (x : V) => true) ∧ ¬s = fun (x : V) => false then 1 else 0

Nonconsensus indicates the configurations that are neither all-white nor all-black.

theorem Voter.iterate_survival {V : Type u_1} [Fintype V] [DecidableEq V] (K : Dynamics.Kernel (Config V Bool)) (n : ℕ) (s : Config V Bool) : K.iterate n survival s = K.event (fun (t : Config V Bool) => (¬t = fun (x : V) => true) ∧ ¬t = fun (x : V) => false) n s

Finite-time nonconsensus as an event.

theorem Voter.survival_nonneg {V : Type u_1} [Fintype V] (s : Config V Bool) : 0 ≤ survival s

theorem Voter.survival_le_one {V : Type u_1} [Fintype V] (s : Config V Bool) : survival s ≤ 1

theorem Voter.transition_constant {V : Type u_1} [Fintype V] [DecidableEq V] {C : Type u_2} [Fintype C] (H : Dynamics.Kernel V) (c : C) (f : Config V C → ℝ) : ((transition H).apply f fun (x : V) => c) = f fun (x : V) => c

Consensus configurations are absorbing.

theorem Voter.survival_step {V : Type u_1} [Fintype V] [DecidableEq V] (H : Dynamics.Kernel V) (s : Config V Bool) : (transition H).apply survival s ≤ survival s

theorem Voter.possible_positive {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (H : Dynamics.Kernel V) (hsupport : ∀ (i j : V), G.Adj i j → 0 < (H i).weight j) {s t : Config V Bool} (h : Possible G s t) : 0 < (transition H s).weight t

Every graph-allowed round has positive probability.

theorem Voter.expect_lt_one {α : Type u_2} [Fintype α] (p : Dynamics.Distribution α) (f : α → ℝ) (hf : ∀ (a : α), f a ≤ 1) (b : α) (hb : 0 < p.weight b) (hfb : f b < 1) : p.expect f < 1

A positive transition to a state with success probability makes success possible here.

theorem Voter.reachable_success {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (H : Dynamics.Kernel V) (hsupport : ∀ (i j : V), G.Adj i j → 0 < (H i).weight j) {s : Config V Bool} {c : Bool} (h : Relation.ReflTransGen (Possible G) s fun (x : V) => c) : ∃ (n : ℕ), (transition H).iterate n survival s < 1

theorem Voter.consensus_tendsto {V : Type u_1} [Fintype V] [DecidableEq 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) (s : Config V Bool) : Filter.Tendsto (fun (n : ℕ) => (transition H).iterate n survival s) Filter.atTop (nhds 0)

Nonconsensus probability tends to zero (Lemma 2.1).