The red-blue pebble game: windows of a calculation, and what dominates them

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 key argument (the proof of their Theorem 3.1), in the form the FFT bound needs and without its partitions. Cut a calculation into windows, each ending once it has made S loads or stores. The vertices given a red pebble in a window are dominated — every path to them from an input meets it — by the at most 2S vertices that were red at the window's start or were loaded in it. So if no set dominated by 2S vertices has more than U elements, a calculation charged q gives red pebbles to at most (q + S) U / S vertices (Trace.mul_card_newReds_le).

Domination is read with paths of length 0 included: an input is dominated only by a set containing it.

def MiscMath.Computability.RedBluePebbleGame.Dominated {V : Type u_1} (E : V → V → Prop) (I D : Finset V) (v : V) : Prop

Dominated E I D v: every path along E from an input to v meets D, paths of length 0 included. A path avoiding D is a chain of edges none of whose endpoints lies in D.

Equations

• MiscMath.Computability.RedBluePebbleGame.Dominated E I D v = ∀ x ∈ I, x ∉ D → ¬Relation.ReflTransGen (fun (a b : V) => E a b ∧ a ∉ D ∧ b ∉ D) x v

theorem MiscMath.Computability.RedBluePebbleGame.dominated_of_mem {V : Type u_1} {E : V → V → Prop} {I D : Finset V} {v : V} (hv : v ∈ D) : Dominated E I D v

theorem MiscMath.Computability.RedBluePebbleGame.Dominated.of_preds {V : Type u_1} {E : V → V → Prop} {I D : Finset V} {v : V} (hvI : v ∉ I) (hp : ∀ (u : V), E u v → Dominated E I D u) : Dominated E I D v

A non-input all of whose predecessors are dominated is dominated.

def MiscMath.Computability.RedBluePebbleGame.Trace.charges {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (j : ℕ) : ℕ

The total charge of the first j moves.

Equations

• T.charges j = ∑ i ∈ Finset.range j, T.c i

theorem MiscMath.Computability.RedBluePebbleGame.Trace.charges_succ {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (j : ℕ) : T.charges (j + 1) = T.charges j + T.c j

theorem MiscMath.Computability.RedBluePebbleGame.Trace.charges_mono {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {j e : ℕ} (h : j ≤ e) : T.charges j ≤ T.charges e

theorem MiscMath.Computability.RedBluePebbleGame.Trace.charges_add_sum_Ico {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {j e : ℕ} (h : j ≤ e) : T.charges j + ∑ i ∈ Finset.Ico j e, T.c i = T.charges e

def MiscMath.Computability.RedBluePebbleGame.Trace.newReds {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (j e : ℕ) : Finset V

The vertices given a red pebble by moves j, …, e - 1.

Equations

• T.newReds j e = (Finset.Ico j e).biUnion fun (i : ℕ) => (T.σ (i + 1)).1 \ (T.σ i).1

def MiscMath.Computability.RedBluePebbleGame.Trace.windowDom {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (j e : ℕ) : Finset V

The dominator of the window of moves j, …, e - 1: the red pebbles at its start, and the vertices it loads.

Equations

• T.windowDom j e = (T.σ j).1 ∪ {i ∈ Finset.Ico j e | T.c i = 1}.biUnion fun (i : ℕ) => (T.σ (i + 1)).1 \ (T.σ i).1

theorem MiscMath.Computability.RedBluePebbleGame.Trace.card_windowDom_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {j e : ℕ} (hj : j ≤ T.t) (he : e ≤ T.t) : (T.windowDom j e).card ≤ S + ∑ i ∈ Finset.Ico j e, T.c i

theorem MiscMath.Computability.RedBluePebbleGame.Trace.dominated_of_mem_window {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {j e : ℕ} (he : e ≤ T.t) (m : ℕ) : j ≤ m → m ≤ e → ∀ v ∈ (T.σ m).1, Dominated E I (T.windowDom j e) v

Every red pebble present during a window is on a vertex its dominator dominates.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.dominated_of_mem_newReds {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {j e : ℕ} (he : e ≤ T.t) {v : V} (hv : v ∈ T.newReds j e) : Dominated E I (T.windowDom j e) v

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mul_card_newReds_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (hS : 1 ≤ S) (U : ℝ) (hU0 : 0 ≤ U) (hU : ∀ (D W : Finset V), D.card ≤ 2 * S → (∀ w ∈ W, Dominated E I D w) → ↑W.card ≤ U) (j : ℕ) : j ≤ T.t → ↑S * ↑(T.newReds j T.t).card ≤ (↑(T.charges T.t) - ↑(T.charges j) + ↑S) * U

Hong and Kung's key argument, without partitions. If no set dominated by at most 2S vertices has more than U elements, then the vertices given a red pebble from move j on number at most (q - charges j + S) U / S, where q is the whole calculation's charge.