Graph-indexed rounds

Round types for dynamics on a finite simple graph G, to be averaged with avg, iterated with expList and turned into kernels with Kernel.ofStep.

• NeighborRound G: a synchronous round in which every vertex samples one of its neighbours. It is the product over the vertices of their neighbour sets, so under the uniform distribution the samples are independent (avg_neighborRound_prod, avg_neighborRound_mul) and each is uniform among the neighbours (avg_neighborRound_eval). On the complete graph this is the round type RumorPush.Tgt n of rumor_spread/. A uniform vertex together with a uniform synchronous round is the sequential "random vertex, random neighbour" step (avg_vertex_neighborRound).
• EdgeRound G: a sequential step in which one oriented edge (a SimpleGraph.Dart) is activated. A uniform oriented edge is a uniform edge (avg_edgeRound_edge) with a uniform orientation (avg_edgeRound_symm); averages over it are sums over adjacent ordered pairs divided by 2 |E| (avg_edgeRound), and its tail is degree-biased (avg_edgeRound_fst).

Uniform averages over the neighbours of v are written avg (fun u : G.neighborSet v => g u), equal to (∑ u ∈ G.neighborFinset v, g u) / G.degree v (avg_neighborSet).

@[reducible, inline]

abbrev Dynamics.NeighborRound {V : Type u_1} (G : SimpleGraph V) : Type u_1

A synchronous round on G: every vertex v picks a neighbour r v. Under the uniform distribution the picks are independent and uniform among the neighbours.

Equations

• Dynamics.NeighborRound G = ((v : V) → ↑(G.neighborSet v))

@[reducible, inline]

abbrev Dynamics.EdgeRound {V : Type u_1} (G : SimpleGraph V) : Type u_1

A sequential step on G: one oriented edge (d.fst, d.snd) of G is activated. Under the uniform distribution this is a uniform edge with a uniform orientation.

Equations

• Dynamics.EdgeRound G = G.Dart

Uniform neighbours and synchronous rounds: every vertex samples a neighbour

theorem Dynamics.avg_neighborSet {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (g : V → ℝ) : (avg fun (u : ↑(G.neighborSet v)) => g ↑u) = (∑ u ∈ G.neighborFinset v, g u) / ↑(G.degree v)

The uniform average over the neighbours of v is their sum divided by the degree.

theorem Dynamics.nonempty_neighborSet {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hd : ∀ (v : V), 0 < G.degree v) (v : V) : Nonempty ↑(G.neighborSet v)

With no isolated vertex, every neighbour set is nonempty.

theorem Dynamics.neighborRound_nonempty {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hd : ∀ (v : V), 0 < G.degree v) : Nonempty (NeighborRound G)

Synchronous rounds exist as soon as no vertex is isolated.

theorem Dynamics.card_neighborRound {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] : Fintype.card (NeighborRound G) = ∏ v : V, G.degree v

The number of synchronous rounds is the product of the degrees.

theorem Dynamics.avg_neighborRound_prod {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (f : V → V → ℝ) : (avg fun (r : NeighborRound G) => ∏ v : V, f v ↑(r v)) = ∏ v : V, avg fun (u : ↑(G.neighborSet v)) => f v ↑u

Independence: in a uniform synchronous round the vertices sample their neighbours independently, so averages of products over the vertices factor.

theorem Dynamics.avg_neighborRound_eval {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (hd : ∀ (v : V), 0 < G.degree v) (v : V) (g : V → ℝ) : (avg fun (r : NeighborRound G) => g ↑(r v)) = avg fun (u : ↑(G.neighborSet v)) => g ↑u

Marginal: in a uniform synchronous round each vertex samples a uniform neighbour.

theorem Dynamics.avg_neighborRound_mul {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (hd : ∀ (v : V), 0 < G.degree v) {v w : V} (hvw : v ≠ w) (g h : V → ℝ) : (avg fun (r : NeighborRound G) => g ↑(r v) * h ↑(r w)) = (avg fun (u : ↑(G.neighborSet v)) => g ↑u) * avg fun (u : ↑(G.neighborSet w)) => h ↑u

Pairwise independence: in a uniform synchronous round two distinct vertices sample their neighbours independently.

theorem Dynamics.avg_neighborRound_sum {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (hd : ∀ (v : V), 0 < G.degree v) (f : V → V → ℝ) : (avg fun (r : NeighborRound G) => ∑ v : V, f v ↑(r v)) = ∑ v : V, avg fun (u : ↑(G.neighborSet v)) => f v ↑u

Linearity over the vertices: the average of a sum of one-vertex observables is the sum of their neighbour averages.

theorem Dynamics.avg_vertex_neighborRound {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (hd : ∀ (v : V), 0 < G.degree v) (F : V → V → ℝ) : (avg fun (p : V × NeighborRound G) => F p.1 ↑(p.2 p.1)) = avg fun (v : V) => avg fun (u : ↑(G.neighborSet v)) => F v ↑u

Random vertex, then random neighbour: a uniform vertex v together with a uniform synchronous round r realizes the sequential step "a uniform vertex v and a uniform neighbour r v of v" (the death–Birth scheduler), so V × NeighborRound G is its round type.

Sequential rounds: one uniformly random oriented edge per step

theorem Dynamics.edgeRound_nonempty {V : Type u_1} (G : SimpleGraph V) {u v : V} (h : G.Adj u v) : Nonempty (EdgeRound G)

Sequential steps exist as soon as G has an edge.

theorem Dynamics.avg_edgeRound_symm {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (F : V → V → ℝ) : (avg fun (d : EdgeRound G) => F d.toProd.2 d.toProd.1) = avg fun (d : EdgeRound G) => F d.toProd.1 d.toProd.2

Uniform orientation: averages are invariant under reversing the activated edge.

theorem Dynamics.avg_edgeRound {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (F : V → V → ℝ) : (avg fun (d : EdgeRound G) => F d.toProd.1 d.toProd.2) = (∑ v : V, ∑ u ∈ G.neighborFinset v, F v u) / (2 * ↑G.edgeFinset.card)

Uniform oriented edge: the average over the activated oriented edge is the sum over the adjacent ordered pairs divided by 2 |E|.

theorem Dynamics.avg_edgeRound_edge {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (g : Sym2 V → ℝ) : (avg fun (d : EdgeRound G) => g (SimpleGraph.Dart.edge d)) = avg fun (e : ↑G.edgeSet) => g ↑e

Uniform edge: the underlying edge of a uniform oriented edge is a uniform edge.

theorem Dynamics.avg_edgeRound_fst {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (g : V → ℝ) : (avg fun (d : EdgeRound G) => g d.toProd.1) = (∑ v : V, ↑(G.degree v) * g v) / (2 * ↑G.edgeFinset.card)

Degree bias: the tail of a uniform oriented edge is v with probability deg v / 2 |E|.