The step matrix of sequential averaging: entries and weighted sums

Helpers for Averaging.Sequential: the entries of W(i, j) = I - (eᵢ - eⱼ)(eᵢ - eⱼ)ᵀ / 2 (Survey, equation (2)), its action on a state, its symmetry and idempotence, the weighted sum ∑ᵢⱼ Qᵢⱼ W(i, j) for an arbitrary weight matrix Q (the common computation behind equation (4) and the uniform-edge identity), and sums over the darts of a graph as sums over adjacent pairs.

theorem Averaging.Sequential.edgeMatrix_apply {V : Type u_1} [DecidableEq V] (i j a b : V) : edgeMatrix i j a b = (if a = b then 1 else 0) - ((if a = i then 1 else 0) - if a = j then 1 else 0) * ((if b = i then 1 else 0) - if b = j then 1 else 0) / 2

The entries of W(i, j): δₐᵦ - (δₐᵢ - δₐⱼ)(δᵦᵢ - δᵦⱼ) / 2.

theorem Averaging.Sequential.edgeMatrix_transpose {V : Type u_1} [DecidableEq V] (i j : V) : (edgeMatrix i j).transpose = edgeMatrix i j

W(i, j) is symmetric.

theorem Averaging.Sequential.edgeMatrix_mulVec_eq {V : Type u_1} [Fintype V] [DecidableEq V] (i j : V) (x : V → ℝ) : (edgeMatrix i j).mulVec x = fun (w : V) => if w = i ∨ w = j then (x i + x j) / 2 else x w

One step on the edge (i, j) averages the values of the two endpoints.

theorem Averaging.Sequential.edgeMatrix_mulVec_mulVec {V : Type u_1} [Fintype V] [DecidableEq V] (i j : V) (x : V → ℝ) : (edgeMatrix i j).mulVec ((edgeMatrix i j).mulVec x) = (edgeMatrix i j).mulVec x

Averaging the same edge twice is averaging it once.

theorem Averaging.Sequential.edgeMatrix_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (i j : V) : edgeMatrix i j * edgeMatrix i j = edgeMatrix i j

W(i, j) is idempotent.

theorem Averaging.Sequential.sum_sum_ite_left_left {V : Type u_1} [Fintype V] [DecidableEq V] (Q : V → V → ℝ) (a b : V) : (∑ i : V, ∑ j : V, (if a = i then Q i j else 0) * if b = i then 1 else 0) = (if a = b then 1 else 0) * ∑ j : V, Q a j

theorem Averaging.Sequential.sum_sum_ite_left_right {V : Type u_1} [Fintype V] [DecidableEq V] (Q : V → V → ℝ) (a b : V) : (∑ i : V, ∑ j : V, (if a = i then Q i j else 0) * if b = j then 1 else 0) = Q a b

theorem Averaging.Sequential.sum_sum_ite_right_left {V : Type u_1} [Fintype V] [DecidableEq V] (Q : V → V → ℝ) (a b : V) : (∑ i : V, ∑ j : V, (if a = j then Q i j else 0) * if b = i then 1 else 0) = Q b a

theorem Averaging.Sequential.sum_sum_ite_right_right {V : Type u_1} [Fintype V] [DecidableEq V] (Q : V → V → ℝ) (a b : V) : (∑ i : V, ∑ j : V, (if a = j then Q i j else 0) * if b = j then 1 else 0) = (if a = b then 1 else 0) * ∑ i : V, Q i a

theorem Averaging.Sequential.sum_mul_edgeMatrix_apply {V : Type u_1} [Fintype V] [DecidableEq V] (Q : V → V → ℝ) (a b : V) : ∑ i : V, ∑ j : V, Q i j * edgeMatrix i j a b = ((∑ i : V, ∑ j : V, Q i j) * if a = b then 1 else 0) - ((if a = b then 1 else 0) * ∑ j : V, (Q a j + Q j a) - Q a b - Q b a) / 2

The weighted sum ∑ᵢⱼ Qᵢⱼ W(i, j), entrywise: the total weight times I, minus half of D̄ - Q - Qᵀ with D̄ₐₐ = ∑ⱼ (Qₐⱼ + Qⱼₐ).

def Averaging.Sequential.dartEquiv {V : Type u_1} (G : SimpleGraph V) : G.Dart ≃ { p : V × V // G.Adj p.1 p.2 }

The darts of G are the adjacent ordered pairs.

Equations

• One or more equations did not get rendered due to their size.

theorem Averaging.Sequential.sum_dart {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (f : V → V → ℝ) : ∑ d : G.Dart, f d.toProd.1 d.toProd.2 = ∑ a : V, ∑ b : V, if G.Adj a b then f a b else 0

A sum over the darts of G is a sum over the adjacent ordered pairs.

theorem Averaging.Sequential.sum_dart_edgeMatrix_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (a b : V) : ∑ d : G.Dart, edgeMatrix d.toProd.1 d.toProd.2 a b = (2 * ↑G.edgeFinset.card * if a = b then 1 else 0) - SimpleGraph.lapMatrix ℝ G a b

∑_{darts} W(d), entrywise: 2m I - L.

theorem Averaging.Sequential.sum_sq_edgeMatrix_mulVec {V : Type u_1} [Fintype V] [DecidableEq V] (i j : V) (x : V → ℝ) : ∑ v : V, (edgeMatrix i j).mulVec x v ^ 2 = x ⬝ᵥ (edgeMatrix i j).mulVec x

The squared norm after one step is the quadratic form of W: ‖W x‖² = xᵀ W x, since W is a symmetric projection.

theorem Averaging.Sequential.avg_edgeMatrix_mulVec_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty G.Dart] (x : V → ℝ) (c : V) (hW : ∀ (a b : V), (Dynamics.avg fun (d : G.Dart) => edgeMatrix d.toProd.1 d.toProd.2 a b) = meanMatrix G a b) : (Dynamics.avg fun (d : G.Dart) => (edgeMatrix d.toProd.1 d.toProd.2).mulVec x c) = (meanMatrix G).mulVec x c

The average of W(d) x over a uniformly random dart is (I - L/(2m)) x.