Documentation

Complexitylib.Algebraic.MassProduction.HighRate.Rate

Rate one with an explicit finite cutoff #

The retained dimension is A^m - (A-1)^m. Bernoulli's inequality gives the integer precision statement precision * A^m <= (precision+1) * dimension as soon as m >= precision * (A-1) and m > 0. No real asymptotic notation or unproved limiting step is needed.

source
def Algebraic.MassProduction.HighRate.retainedDimension (alphabet blocks : ℕ) :
ℕ

Exact size of the family containing an all-zero digit column.

Equations
Instances For
    source
    theorem Algebraic.MassProduction.HighRate.retainedDimension_rate (alphabet blocks precision : ℕ) (alphabetPositive : 0 < alphabet) (blocksPositive : 0 < blocks) (blocksLarge : precision * (alphabet - 1) ≤ blocks) :
    precision * alphabet ^ blocks ≤ (precision + 1) * retainedDimension alphabet blocks

    A finite rate guarantee, with an explicit cutoff linear in precision.

    source
    theorem Algebraic.MassProduction.HighRate.retainedDimension_hasRateOne (alphabet : ℕ) (alphabetPositive : 0 < alphabet) (precision : ℕ) :
    ∃ (cutoff : ℕ), ∀ (blocks : ℕ), cutoff ≤ blocks → precision * alphabet ^ blocks ≤ (precision + 1) * retainedDimension alphabet blocks

    The dimension approaches the full table size in the integer precision form used by the circuit-cost statements.