The red-blue pebble game: the function d · log₂ (2d)

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.

bfly d = d · log₂ (2d) bounds the number of vertices of the FFT graph that d vertices can dominate (Butterfly.lean). It sharpens Hong and Kung's 2d log d, which they claim for d ≥ 2 and which is 0 at d = 1, where a single vertex dominates itself, although their induction applies it there; bfly 1 = 1. This file proves the inequalities that induction needs, the step being bfly_combine, from log₂ (1 + t) ≥ t on [0, 1], which is concavity of log (the paper's lemma H(p) ≥ 2p on [0, ½] in another form).

noncomputable def MiscMath.Computability.RedBluePebbleGame.bfly (d : ℕ) : ℝ

The butterfly bound d · log₂ (2d); its value at d = 0 is 0.

Equations

• MiscMath.Computability.RedBluePebbleGame.bfly d = ↑d * Real.logb 2 (2 * ↑d)

theorem MiscMath.Computability.RedBluePebbleGame.bfly_zero : bfly 0 = 0

theorem MiscMath.Computability.RedBluePebbleGame.bfly_one : bfly 1 = 1

theorem MiscMath.Computability.RedBluePebbleGame.bfly_nonneg (d : ℕ) : 0 ≤ bfly d

theorem MiscMath.Computability.RedBluePebbleGame.bfly_mono {a b : ℕ} (h : a ≤ b) : bfly a ≤ bfly b

theorem MiscMath.Computability.RedBluePebbleGame.bfly_combine (a b c : ℕ) : bfly a + bfly b + ↑c + 2 * ↑(min a b) ≤ bfly (a + b + c)

The step of the butterfly induction.

theorem MiscMath.Computability.RedBluePebbleGame.bfly_two_mul (S : ℕ) : bfly (2 * S) = 2 * ↑S * Real.logb 2 (4 * ↑S)