The red-blue pebble game: how much of the FFT graph d vertices can dominate

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.

card_le_bfly_of_dominated: in the 2^k-point FFT graph, a set of vertices dominated by D has at most |D| · log₂ (2|D|) elements. This is the argument of Hong and Kung's Theorem 4.1, with a sharper bound that repairs its induction: they claim 2d log₂ d for d ≥ 2, which follows, but their induction also applies it to parts of a dominator with a single vertex, where it is 0 although a single vertex dominates itself.

The induction runs over the sub-butterflies of the fixed graph. The one of height L numbered β (InBlock L β) has the levels up to L and the lanes whose bits from L up spell β. It splits into two sub-butterflies of height L - 1, A and B, and its top level C. Each vertex of C not in the dominator has one straight path to it through A and one through B. The straight paths through A of vertices in distinct lanes of A are disjoint, and at most two vertices of C share a lane of A. So at most 2|D ∩ A| of them, and likewise at most 2|D ∩ B|, escape the dominator.

Bits

theorem MiscMath.Computability.RedBluePebbleGame.xor_two_pow_xor_two_pow (x L : ℕ) : x ^^^ 2 ^ L ^^^ 2 ^ L = x

theorem MiscMath.Computability.RedBluePebbleGame.testBit_xor_two_pow_self (x L : ℕ) : (x ^^^ 2 ^ L).testBit L = !x.testBit L

theorem MiscMath.Computability.RedBluePebbleGame.xor_two_pow_div (x L : ℕ) : (x ^^^ 2 ^ L) / 2 ^ (L + 1) = x / 2 ^ (L + 1)

theorem MiscMath.Computability.RedBluePebbleGame.div_two_pow_eq (x L : ℕ) : x / 2 ^ L = 2 * (x / 2 ^ (L + 1)) + if x.testBit L = true then 1 else 0

theorem MiscMath.Computability.RedBluePebbleGame.xor_two_pow_lt {x L k : ℕ} (hx : x < 2 ^ k) (hL : L < k) : x ^^^ 2 ^ L < 2 ^ k

Sub-butterflies

@[reducible, inline]

abbrev MiscMath.Computability.RedBluePebbleGame.InBlock {k : ℕ} (L β : ℕ) (v : Fin (k + 1) × Fin (2 ^ k)) : Prop

v lies in the sub-butterfly of height L numbered β: at a level at most L, in a lane whose bits from L up spell β.

Equations

• MiscMath.Computability.RedBluePebbleGame.InBlock L β v = (↑v.1 ≤ L ∧ ↑v.2 / 2 ^ L = β)

theorem MiscMath.Computability.RedBluePebbleGame.straight_path {k : ℕ} (D : Finset (Fin (k + 1) × Fin (2 ^ k))) (y : Fin (2 ^ k)) (l : ℕ) (hl : l ≤ k) : (∀ (v : Fin (k + 1) × Fin (2 ^ k)), v.2 = y → ↑v.1 ≤ l → v ∉ D) → Relation.ReflTransGen (fun (a b : Fin (k + 1) × Fin (2 ^ k)) => fftEdge k a b ∧ a ∉ D ∧ b ∉ D) (⟨0, ⋯⟩, y) (⟨l, ⋯⟩, y)

A straight path up lane y, from level 0 to level l, avoiding D if the lane does below level l.

theorem MiscMath.Computability.RedBluePebbleGame.card_escaping_le {k : ℕ} (D W : Finset (Fin (k + 1) × Fin (2 ^ k))) (L β : ℕ) (hL : L + 1 ≤ k) (b : Bool) (hW : ∀ w ∈ W, ↑w.1 = L + 1 ∧ ↑w.2 / 2 ^ (L + 1) = β ∧ w ∉ D) (hdom : ∀ w ∈ W, Dominated (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} D w) : W.card ≤ 2 * (Finset.filter (InBlock L (2 * β + if b = true then 1 else 0)) D).card

The vertices of the top level of a sub-butterfly that escape the dominator: at most twice the number of dominator vertices in either half below.

theorem MiscMath.Computability.RedBluePebbleGame.card_le_bfly_of_inBlock {k : ℕ} (D : Finset (Fin (k + 1) × Fin (2 ^ k))) (L : ℕ) : L ≤ k → ∀ (β : ℕ) (W : Finset (Fin (k + 1) × Fin (2 ^ k))), (∀ w ∈ W, InBlock L β w) → (∀ w ∈ W, Dominated (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} D w) → ↑W.card ≤ bfly (Finset.filter (InBlock L β) D).card

The domination bound on one sub-butterfly, by induction on its height.

theorem MiscMath.Computability.RedBluePebbleGame.card_le_bfly_of_dominated {k : ℕ} {D W : Finset (Fin (k + 1) × Fin (2 ^ k))} (hW : ∀ w ∈ W, Dominated (fftEdge k) {x : Fin (k + 1) × Fin (2 ^ k) | x.1 = 0} D w) : ↑W.card ≤ bfly D.card

The domination bound. In the 2^k-point FFT graph, a set of vertices dominated by D has at most |D| · log₂ (2|D|) elements (none if D is empty).