The red-blue pebble game: the two I/O bounds for the FFT graph

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.

In a complete calculation of the 2^k-point FFT graph every vertex holds a red pebble at some point (fft_exists_red): the outputs end blue, the first pebble on a non-input comes from computing it, and computing a vertex needs its predecessors red. Two bounds follow:

• fft_two_pow_succ_le: each of the 2^k inputs is loaded and each of the 2^k outputs stored, so q ≥ 2^(k+1);
• fft_mul_card_le: Hong and Kung's key argument (Trace.mul_card_newReds_le) with the domination bound for the FFT graph (card_le_bfly_of_dominated) gives S · (k + 1) 2^k ≤ (q + S) · 2S log₂ (4S).

@[instance_reducible]

instance MiscMath.Computability.RedBluePebbleGame.fftEdge.decidableRel (k : ℕ) : DecidableRel (fftEdge k)

The butterfly's edges can be decided, which lets concrete calculations be checked by decide.

Equations

• MiscMath.Computability.RedBluePebbleGame.fftEdge.decidableRel k u v = id inferInstance

theorem MiscMath.Computability.RedBluePebbleGame.card_filter_fst_eq {k : ℕ} (a : Fin (k + 1)) : {v : Fin (k + 1) × Fin (2 ^ k) | v.1 = a}.card = 2 ^ k

The vertices of one level of the FFT graph number 2^k.

theorem MiscMath.Computability.RedBluePebbleGame.fft_exists_red {k S : ℕ} (hk : 1 ≤ k) (T : Trace (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} S) (h0 : T.σ 0 = (∅, {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0})) (ht : T.σ T.t = (∅, {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = Fin.last k})) (v : Fin (k + 1) × Fin (2 ^ k)) : ∃ j ≤ T.t, v ∈ (T.σ j).1

In a complete calculation of the FFT graph, every vertex holds a red pebble at some point.

theorem MiscMath.Computability.RedBluePebbleGame.fft_two_pow_succ_le {k S q : ℕ} (hk : 1 ≤ k) (h : HasCompleteCalculation (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = Fin.last k} S q) : 2 ^ (k + 1) ≤ q

The trivial bound. Every input is loaded and every output stored: q ≥ 2^(k+1).

theorem MiscMath.Computability.RedBluePebbleGame.fft_mul_card_le {k S q : ℕ} (hk : 1 ≤ k) (hS : 1 ≤ S) (h : HasCompleteCalculation (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = Fin.last k} S q) : ↑S * ((↑k + 1) * 2 ^ k) ≤ (↑q + ↑S) * (2 * ↑S * Real.logb 2 (4 * ↑S))

The domination bound on I/O. S · (k + 1) 2^k ≤ (q + S) · 2S log₂ (4S).