Synchronous weighted voter dynamics (Section 2.1)

Each vertex independently samples one row of the stochastic matrix and copies that neighbor's previous color. Colors need not be Boolean.

@[reducible, inline]

abbrev Voter.Config (V : Type u_4) (C : Type u_5) : Type (max u_4 u_5)

A configuration assigns a color to each vertex.

Equations

• Voter.Config V C = (V → C)

def Voter.step {V : Type u_1} {C : Type u_2} (s : Config V C) (r : V → V) : Config V C

Simultaneous copying for a fixed vector of sampled neighbors.

Equations

• Voter.step s r i = s (r i)

@[simp]

theorem Voter.step_constant {V : Type u_1} {C : Type u_2} (c : C) (r : V → V) : step (fun (x : V) => c) r = fun (x : V) => c

theorem Voter.step_project {V : Type u_1} {C : Type u_2} {D : Type u_3} (f : C → D) (s : Config V C) (r : V → V) : step (f ∘ s) r = f ∘ step s r

Color projections commute with every realization of a round.

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

Expected observable after independently sampling one neighbor per vertex.

Equations

• Voter.round H s f = (Dynamics.Distribution.independent H).expect fun (r : V → V) => f (Voter.step s r)

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

The configuration transition kernel is the pushforward of independent sampling.

Equations

• Voter.transition H s = (Dynamics.Distribution.independent H).map (Voter.step s)

theorem Voter.transition_apply {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (s : Config V C) (f : Config V C → ℝ) : (transition H).apply f s = round H s f

theorem Voter.round_eval {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] (H : Dynamics.Kernel V) (s : Config V C) (i : V) (f : C → ℝ) : (round H s fun (t : Config V C) => f (t i)) = (H i).expect fun (j : V) => f (s j)

One coordinate has precisely the distribution of its sampled neighbor.

theorem Voter.round_prod {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] (H : Dynamics.Kernel V) (s : Config V C) (f : V → C → ℝ) : (round H s fun (t : Config V C) => ∏ i : V, f i (t i)) = ∏ i : V, (H i).expect fun (j : V) => f i (s j)

Product observables factor over the independently updated vertices.

theorem Voter.transition_product {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (s t : Config V C) : (transition H s).weight t = ∏ i : V, (H i).prob fun (j : V) => s j = t i

The product formula for the probability of a configuration (Section 2.1).

theorem Voter.transition_product_bool {V : Type u_1} [Fintype V] [DecidableEq V] (H : Dynamics.Kernel V) (s t : Config V Bool) : (transition H s).weight t = ∏ i : V, if t i = true then (H i).expect fun (j : V) => if s j = true then 1 else 0 else 1 - (H i).expect fun (j : V) => if s j = true then 1 else 0

The Boolean white/black factorization displayed in Section 2.1.

noncomputable def Voter.mass {V : Type u_1} {C : Type u_2} [Fintype V] (p : Dynamics.Distribution V) (f : C → ℝ) (s : Config V C) : ℝ

Weighted color mass for any real-valued color observable.

Equations

• Voter.mass p f s = p.expect fun (i : V) => f (s i)

theorem Voter.round_mass {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] (H : Dynamics.Kernel V) (p : Dynamics.Distribution V) (hp : H.Stationary p) (f : C → ℝ) (s : Config V C) : round H s (mass p f) = mass p f s

Stationary mass is preserved by one round, without graph assumptions (Lemma 2.3).

theorem Voter.iterate_mass {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] [Fintype C] (H : Dynamics.Kernel V) (p : Dynamics.Distribution V) (hp : H.Stationary p) (f : C → ℝ) (n : ℕ) (s : Config V C) : (transition H).iterate n (mass p f) s = mass p f s

Iterated stationary-mass preservation (Lemma 2.3).