Averaging dynamics on graphs

In every round each node replaces its value by the average of its neighbours' values (the expectation of the value at one step of the random walk). The degree-weighted sum of the values is conserved, values stay within the initial range, and on a connected graph containing an odd closed walk (i.e. a connected non-bipartite graph) every node's value converges to the degree-weighted average ∑ deg v · x v / ∑ deg v of the initial values. On a connected bipartite graph with at least two nodes this fails: the values ±1 of a proper 2-colouring alternate forever.

noncomputable def Averaging.avgStep {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : V → ℝ

One round of averaging: every node takes the average of its neighbours' values.

Equations

• Averaging.avgStep G x v = (∑ u ∈ G.neighborFinset v, x u) / ↑(G.degree v)

noncomputable def Averaging.avgIter {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ → (V → ℝ) → V → ℝ

t rounds of averaging.

Equations

• Averaging.avgIter G 0 x✝ = x✝
• Averaging.avgIter G t.succ x✝ = Averaging.avgStep G (Averaging.avgIter G t x✝)

noncomputable def Averaging.degAvg {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : ℝ

The degree-weighted average of the values (their mean under the stationary distribution of the random walk).

Equations

• Averaging.degAvg G x = (∑ v : V, ↑(G.degree v) * x v) / ∑ v : V, ↑(G.degree v)

Conservation and the maximum principle

theorem Averaging.degree_mul_avgStep {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) (v : V) : ↑(G.degree v) * avgStep G x v = ∑ u ∈ G.neighborFinset v, x u

theorem Averaging.sum_sum_neighbor_comm {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (f : V → V → ℝ) : ∑ u : V, ∑ w ∈ G.neighborFinset v, f w u = ∑ w ∈ G.neighborFinset v, ∑ u : V, f w u

Swap a sum over neighbours of v with a sum over all vertices.

theorem Averaging.sum_sum_neighbor {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : ∑ v : V, ∑ u ∈ G.neighborFinset v, x u = ∑ u : V, ↑(G.degree u) * x u

theorem Averaging.degree_weighted_sum_step {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : ∑ v : V, ↑(G.degree v) * avgStep G x v = ∑ v : V, ↑(G.degree v) * x v

The degree-weighted sum is conserved by a round.

theorem Averaging.avgStep_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) {x : V → ℝ} {M : ℝ} (hM : ∀ (v : V), x v ≤ M) (v : V) : avgStep G x v ≤ M

Maximum principle: without isolated nodes, a round never exceeds an upper bound.

theorem Averaging.le_avgStep {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) {x : V → ℝ} {m : ℝ} (hm : ∀ (v : V), m ≤ x v) (v : V) : m ≤ avgStep G x v

Minimum principle: without isolated nodes, a round never goes below a lower bound.

Transition weights of the random walk

theorem Averaging.sup'_irrel {β : Type u_2} {α : Type u_3} [SemilatticeSup α] {s : Finset β} (H₁ H₂ : s.Nonempty) (f : β → α) : s.sup' H₁ f = s.sup' H₂ f

theorem Averaging.inf'_irrel {β : Type u_2} {α : Type u_3} [SemilatticeInf α] {s : Finset β} (H₁ H₂ : s.Nonempty) (f : β → α) : s.inf' H₁ f = s.inf' H₂ f

theorem Averaging.degree_weighted_sum_iter {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℕ) (x : V → ℝ) : ∑ v : V, ↑(G.degree v) * avgIter G t x v = ∑ v : V, ↑(G.degree v) * x v

theorem Averaging.avgIter_add {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (s t : ℕ) (x : V → ℝ) : avgIter G (t + s) x = avgIter G s (avgIter G t x)

noncomputable def Averaging.transW {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ → V → V → ℝ

Probability of going from v to u in exactly t steps of the random walk.

Equations

• Averaging.transW G 0 x✝¹ x✝ = if x✝¹ = x✝ then 1 else 0
• Averaging.transW G t.succ x✝¹ x✝ = (∑ w ∈ G.neighborFinset x✝¹, Averaging.transW G t w x✝) / ↑(G.degree x✝¹)

theorem Averaging.transW_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℕ) (v u : V) : 0 ≤ transW G t v u

theorem Averaging.transW_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) (t : ℕ) (v : V) : ∑ u : V, transW G t v u = 1

theorem Averaging.avgIter_eq_sum_transW {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℕ) (x : V → ℝ) (v : V) : avgIter G t x v = ∑ u : V, transW G t v u * x u

theorem Averaging.transW_pos_of_walk {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) {t : ℕ} {v u : V} (p : G.Walk v u) (hp : p.length = t) : 0 < transW G t v u

Walks of one common length

theorem Averaging.degree_pos_of_connected_odd {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (a : V) (p : G.Walk a a), Odd p.length) (v : V) : 0 < G.degree v

def Averaging.roundTrip {V : Type u_1} (G : SimpleGraph V) {u w : V} (h : G.Adj u w) : ℕ → G.Walk u u

k trips back and forth along an edge, a closed walk of length 2k.

Equations

• Averaging.roundTrip G h 0 = SimpleGraph.Walk.nil
• Averaging.roundTrip G h k.succ = (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)).append (Averaging.roundTrip G h k)

theorem Averaging.roundTrip_length {V : Type u_1} (G : SimpleGraph V) {u w : V} (h : G.Adj u w) (k : ℕ) : (roundTrip G h k).length = 2 * k

theorem Averaging.exists_walk_add_even {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {v u : V} (p : G.Walk v u) (hdeg : 0 < G.degree u) (k : ℕ) : ∃ (q : G.Walk v u), q.length = p.length + 2 * k

theorem Averaging.exists_uniform_walk_length {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (a : V) (p : G.Walk a a), Odd p.length) : ∃ (L : ℕ), 0 < L ∧ ∀ (v u : V), ∃ (p : G.Walk v u), p.length = L

Range of a configuration

noncomputable def Averaging.fMax {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : ℝ

Equations

• Averaging.fMax f = Finset.univ.sup' ⋯ f

noncomputable def Averaging.fMin {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : ℝ

Equations

• Averaging.fMin f = Finset.univ.inf' ⋯ f

theorem Averaging.le_fMax {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) (v : V) : f v ≤ fMax f

theorem Averaging.fMin_le {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) (v : V) : fMin f ≤ f v

theorem Averaging.exists_eq_fMax {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : ∃ (v : V), fMax f = f v

theorem Averaging.exists_eq_fMin {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : ∃ (v : V), fMin f = f v

theorem Averaging.fMin_le_fMax {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : fMin f ≤ fMax f

theorem Averaging.fMax_avgStep_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (x : V → ℝ) : fMax (avgStep G x) ≤ fMax x

theorem Averaging.le_fMin_avgStep {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (x : V → ℝ) : fMin x ≤ fMin (avgStep G x)

theorem Averaging.fMax_antitone {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (x : V → ℝ) : Antitone fun (t : ℕ) => fMax (avgIter G t x)

theorem Averaging.fMin_monotone {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (x : V → ℝ) : Monotone fun (t : ℕ) => fMin (avgIter G t x)

noncomputable def Averaging.transWMin {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] (t : ℕ) : ℝ

Equations

• Averaging.transWMin G t = Finset.univ.inf' ⋯ fun (p : V × V) => Averaging.transW G t p.1 p.2

theorem Averaging.transWMin_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] (t : ℕ) (v u : V) : transWMin G t ≤ transW G t v u

theorem Averaging.transWMin_pos {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] {t : ℕ} (h : ∀ (v u : V), 0 < transW G t v u) : 0 < transWMin G t

theorem Averaging.range_avgIter_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (L : ℕ) (δ : ℝ) (hδ : ∀ (v u : V), δ ≤ transW G L v u) (y : V → ℝ) : fMax (avgIter G L y) - fMin (avgIter G L y) ≤ (1 - ↑(Fintype.card V) * δ) * (fMax y - fMin y)

Doeblin: a stochastic kernel bounded below by δ contracts the range by 1 - |V| δ.

theorem Averaging.gap_iter {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hdeg : ∀ (v : V), 0 < G.degree v) [Nonempty V] (L : ℕ) (δ : ℝ) (hδ : ∀ (v u : V), δ ≤ transW G L v u) (hρ : 0 ≤ 1 - ↑(Fintype.card V) * δ) (x : V → ℝ) (k : ℕ) : fMax (avgIter G (k * L) x) - fMin (avgIter G (k * L) x) ≤ (1 - ↑(Fintype.card V) * δ) ^ k * (fMax x - fMin x)

theorem Averaging.tendsto_degAvg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hodd : ∃ (u : V) (p : G.Walk u u), Odd p.length) (x : V → ℝ) (v : V) : Filter.Tendsto (fun (t : ℕ) => avgIter G t x v) Filter.atTop (nhds (degAvg G x))

Convergence: on a connected graph with an odd closed walk, every value converges to the degree-weighted average of the initial values.

theorem Averaging.not_tendsto_of_colorable {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nontrivial V] (hc : G.Connected) (h2 : G.Colorable 2) : ∃ (x : V → ℝ), ∀ (v : V), ¬∃ (c : ℝ), Filter.Tendsto (fun (t : ℕ) => avgIter G t x v) Filter.atTop (nhds c)

The odd closed walk is needed: on a connected bipartite graph with at least two nodes, some initial values make no node converge.