The red-blue pebble game: how many parts a dominator partition of the FFT graph needs

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 Theorem 4.1, with a sharper constant than their proof gives. Each part of an S-dominator partition of the 2^k-point FFT graph is dominated by at most S vertices, so it has at most S log₂ (2S) of them (card_le_bfly_of_dominated), and the parts add up to all (k + 1) 2^k vertices (fft_card_le_mul_bfly). The single vertices, taken level by level, are an S-dominator partition for every S ≥ 1 (fft_exists_isDominatorPartition), so the least number of parts is attained there.

theorem MiscMath.Computability.RedBluePebbleGame.card_eq_sum_of_existsUnique {V : Type u_1} [Fintype V] {h : ℕ} {P : Fin h → Finset V} (hP : ∀ (v : V), ∃! i : Fin h, v ∈ P i) : Fintype.card V = ∑ i : Fin h, (P i).card

The parts of a partition add up to the whole.

theorem MiscMath.Computability.RedBluePebbleGame.fft_card_le_mul_bfly {k S h : ℕ} {P : Fin h → Finset (Fin (k + 1) × Fin (2 ^ k))} (hP : IsDominatorPartition (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} S P) : (↑k + 1) * 2 ^ k ≤ ↑h * bfly S

Theorem 4.1, with a sharper constant. The parts of an S-dominator partition of the 2^k-point FFT graph number at least (k + 1) 2^k / (S log₂ (2S)).

theorem MiscMath.Computability.RedBluePebbleGame.fft_exists_isDominatorPartition (k : ℕ) {S : ℕ} (hS : 1 ≤ S) : ∃ (P : Fin ((k + 1) * 2 ^ k) → Finset (Fin (k + 1) × Fin (2 ^ k))), IsDominatorPartition (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} S P

The single vertices of the FFT graph, in the order of their levels, are an S-dominator partition for every S ≥ 1: each dominates itself, and edges run from a level to the next.

theorem MiscMath.Computability.RedBluePebbleGame.fft_isComputationDAG {k : ℕ} (hk : 1 ≤ k) : IsComputationDAG (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = Fin.last k}

The FFT graph is a computation DAG for every k ≥ 1: edges raise the level by one, the inputs (level 0) are the vertices with no predecessor, the vertices with no successor are the outputs (level k), and the two levels differ. So the key lemma applies to it.