Numerical cost bounds for shared band preparation

Main definitions

• BandPreparation.timeBound: a uniform budget for all setup, tables, input copying, band preparation, shared encoder calls and catalogue copies.

Main results

• BandPreparation.thin_timeBound: its explicit finite thin-regime bound. This numerical lemma is separate from the theorem connecting the budget to the actual native execution.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.timeBound (L m N : ℕ) : ℕ

Generic numerical instruction budget; a final halt is charged separately.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.thin_timeBound (m N : ℕ) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) : ↑(timeBound (19 * m) m N) ≤ 40960 * ↑(19 * m + 1) * ↑(MatrixMultiplication.Schonhage.D m) ^ (-(1 / 18)) * ↑N ^ 2

At L=19m, all original input and table overhead is absorbed by the saving for shared encodings. The displayed constants and polynomial exponent are fixed and positive.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.thin_timeBound_div (m N : ℕ) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) : ↑(timeBound (19 * m) m N) ≤ 40960 * ↑(19 * m + 1) * ↑N ^ 2 / ↑(MatrixMultiplication.Schonhage.D m) ^ (1 / 18)

Equivalent division form of the thin-regime bound requested by the matrix algorithm.