Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Cost

Complete native queried-product instruction ledger #

Main definitions #

Every term is derived from ordinary original inputs and the finite pruned trace definition. No solver or running-time assertion is supplied as an input field.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.timeBound {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) :
ℕ

A uniform instruction bound for either original signed inputs or raw nonnegative inputs. The raw-conversion envelope charges a multiplication for every original matrix entry.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.sum_tileCharge {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) :
    ∑ t ∈ Finset.range (MatrixMultiplication.Schonhage.numBands L m N ^ 2), tileCharge hm qs t = (4 * L + 66) * MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 29 * qs.length + ∑ T ∈ MatrixMultiplication.Schonhage.tiles L m N, PrunedQuery.traceWeight (MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm) qs.toFinset T.1 T.2)

    The exact sum of occurrence-dependent call charges uses every original request once. It uses no distinct-set bound on list multiplicity.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.sum_traceWeight_le {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) :
    ∑ T ∈ MatrixMultiplication.Schonhage.tiles L m N, PrunedQuery.traceWeight (MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm) qs.toFinset T.1 T.2) ≤ 8192 * (L + 1) * ∑ T ∈ MatrixMultiplication.Schonhage.tiles L m N, (MatrixMultiplication.Schonhage.leaves (MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm) qs.toFinset T.1 T.2)).card + 4096 * MatrixMultiplication.Schonhage.numBands L m N ^ 2

    Sum the actual native kernel trace charges using the existing contributing-leaf bound.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.timeBound_le {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) :
    timeBound hm qs + 1 ≤ 65536 * (L + 1) * (1 + N * MatrixMultiplication.Schonhage.D m + qs.length + 2 ^ L + (MatrixMultiplication.Schonhage.numBands L m N + 1) * 10 ^ L + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + ∑ T ∈ MatrixMultiplication.Schonhage.tiles L m N, (MatrixMultiplication.Schonhage.leaves (MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm) qs.toFinset T.1 T.2)).card)

    Every actual phase, including halt, is bounded by original input size, shared encodings, tile count and contributing leaves. In particular, repeated requests retain a charged term.