The red-blue pebble game: the I/O bounds for matrix multiplication

Support module of MiscMath.Computability.RedBluePebbleGame, where the results are stated and where the reader should start. Nothing here is a result on its own.

This is Hong and Kung's §6 for the graphs of IsMatMulEvaluation, by way of their Theorem 3.1. A complete calculation with S red pebbles gives a 2S-partition into h parts, S h ≤ q + S (exists_isPartition). Each part holds at most S √(2S) products (card_prod_mem_le, which takes the place of the source's Lemma 6.1):

• a product in the part leads, inside the part, to a vertex with no successor there, which lies in the part's minimum set; products for different entries of the result lead to different such vertices (independent), so the part meets at most 2S entries of the result;
• a product in the part is in its dominator, or both its factors are;
• so, slice by slice in the inner index l, the products of the part outside the dominator number at most min(2S, α_l β_l) ≤ √(2S) (α_l + β_l) / 2, where α_l and β_l count the entries of column l of A and of row l of B in the dominator.

Summing over the parts gives m k n ≤ (q + S) √(2S) (mul_le_of_isMatMulLabelling). Alongside it: every input is loaded and every output stored, so q ≥ m k + k n + m n (add_le_of_isMatMulLabelling), and a calculation needs three red pebbles as soon as there is a product (IsMatMulLabelling.three_le).

Facts about a complete calculation of a computation DAG

theorem MiscMath.Computability.RedBluePebbleGame.IsComputationDAG.exists_succ_of_mem {V : Type u_1} {E : V → V → Prop} {I O : Finset V} [Finite V] (hG : IsComputationDAG E I O) {x : V} (hx : x ∈ I) : ∃ (w : V), E x w

An input of a computation DAG has a successor: it reaches an output, and it is not one.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_pebbled {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} {S : ℕ} (T : Trace E I S) [Finite V] (hG : IsComputationDAG E I O) (h0 : T.σ 0 = (∅, I)) (ht : T.σ T.t = (∅, O)) (v : V) : ∃ j ≤ T.t, v ∈ (T.σ j).1 ∨ v ∈ (T.σ j).2

In a complete calculation of a computation DAG, every vertex holds a pebble at some point: it reaches an output, which ends blue, and a vertex is computed only once its predecessors are red.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_red_of_edge {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} {S : ℕ} (T : Trace E I S) [Finite V] (hG : IsComputationDAG E I O) (h0 : T.σ 0 = (∅, I)) (ht : T.σ T.t = (∅, O)) {u v : V} (huv : E u v) : ∃ i ≤ T.t, u ∈ (T.σ i).1

In a complete calculation of a computation DAG, a vertex with a successor holds a red pebble at some point: the successor is computed, and then it is red.

Facts about a matrix-multiplication labelling

theorem MiscMath.Computability.RedBluePebbleGame.IsMatMulLabelling.prod_notMem {V : Type u_1} {E : V → V → Prop} {I O : Finset V} {m k n : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (x : Fin m × Fin k × Fin n) : p x ∉ I

A product is not an input: it has a predecessor.

theorem MiscMath.Computability.RedBluePebbleGame.IsMatMulLabelling.prod_ne_a {V : Type u_1} {E : V → V → Prop} {I O : Finset V} {m k n : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (x : Fin m × Fin k × Fin n) (y : Fin m × Fin k) : p x ≠ a y

theorem MiscMath.Computability.RedBluePebbleGame.IsMatMulLabelling.prod_ne_b {V : Type u_1} {E : V → V → Prop} {I O : Finset V} {m k n : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (x : Fin m × Fin k × Fin n) (z : Fin k × Fin n) : p x ≠ b z

theorem MiscMath.Computability.RedBluePebbleGame.IsMatMulLabelling.a_ne_b {V : Type u_1} {E : V → V → Prop} {I : Finset V} {m k n : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hL : IsMatMulLabelling E I a b p) (y : Fin m × Fin k) (z : Fin k × Fin n) : a y ≠ b z

theorem MiscMath.Computability.RedBluePebbleGame.IsMatMulLabelling.three_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} {m k n : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} [Finite V] {S q : ℕ} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (x : Fin m × Fin k × Fin n) (hq : HasCompleteCalculation E I O S q) : 3 ≤ S

Three red pebbles are needed. When a product is first computed, it and its two factors are all red.

The trivial bound

theorem MiscMath.Computability.RedBluePebbleGame.add_le_of_isMatMulLabelling {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} [Finite V] {m k n S q : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (hk : 1 ≤ k) (hq : HasCompleteCalculation E I O S q) : m * k + k * n + m * n ≤ q

Every input is loaded and every output stored. The entries of the two matrices are distinct inputs, and for k ≥ 1 the entries of the result lead to distinct outputs, so a complete calculation is charged q ≥ m k + k n + m n.

The products in one part

theorem MiscMath.Computability.RedBluePebbleGame.exists_sink_in {V : Type u_1} {E : V → V → Prop} [Finite V] (hE : ∀ (v : V), ¬Relation.TransGen E v v) {U : Finset V} {v : V} (hv : v ∈ U) : ∃ w ∈ U, Relation.ReflTransGen E v w ∧ ∀ w' ∈ U, ¬E w w'

In a finite graph with no cycle, a vertex of a set U leads, along edges inside U, to a vertex of U with no successor in U.

theorem MiscMath.Computability.RedBluePebbleGame.le_sqrt_mul_add_div_two {t α β s : ℝ} (ht : 0 ≤ t) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hs : 0 ≤ s) (h₁ : t ≤ s) (h₂ : t ≤ α * β) : t ≤ √s * (α + β) / 2

One slice of the count: at most min(s, α β) things, where α β bounds them one way and s another, number at most √s (α + β) / 2.

theorem MiscMath.Computability.RedBluePebbleGame.card_prod_mem_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} [Finite V] {m k n s : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (hs : 4 ≤ s) {U D M : Finset V} (hD : D.card ≤ s) (hDom : Dominates E I D U) (hM : ∀ v ∈ U, (∀ w ∈ U, ¬E v w) → v ∈ M) (hMs : M.card ≤ s) : ↑{x : Fin m × Fin k × Fin n | p x ∈ U}.card ≤ ↑s * √↑s / 2

The products in one part, the source's Lemma 6.1 in the form the proof needs. A set U dominated by at most s ≥ 4 vertices, of which at most s have no successor in U, holds at most s √s / 2 products.

All the products

theorem MiscMath.Computability.RedBluePebbleGame.mul_le_of_isMatMulLabelling {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} [Finite V] {m k n S q : ℕ} {a : Fin m × Fin k → V} {b : Fin k × Fin n → V} {p : Fin m × Fin k × Fin n → V} (hG : IsComputationDAG E I O) (hL : IsMatMulLabelling E I a b p) (hS : 2 ≤ S) (hq : HasCompleteCalculation E I O S q) : ↑m * ↑k * ↑n ≤ (↑q + ↑S) * √(2 * ↑S)

The domination bound, Hong and Kung's Corollary 6.2 in finitary form. A complete calculation with S ≥ 2 red pebbles, charged q, has m k n ≤ (q + S) √(2S).