OAI/Combinatorics/ContingencyTables/Dense/DenseBitBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the manuscript's bounded dense random-bit budget

  1. theorem OAI.ContingencyTables.GridBoundary.denseStepBits_upper line 10
  2. theorem OAI.ContingencyTables.GridBoundary.denseOffsetBits_upper line 17
  3. def OAI.ContingencyTables.GridBoundary.denseRandomBitBudget line 24
  4. theorem OAI.ContingencyTables.GridBoundary.denseRandomBitBudget_polynomial line 30

    Source documentation

    The fixed declared number of dense random bits is polynomial in the dimension parameter, binary margin length, and requested precision.

    theorem denseRandomBitBudget_polynomial (d b h : ℕ) :
    denseRandomBitBudget d b h ≤ 25 * (d + b + h + 1) ^ 62 := by
…

    Mentions: OAI.ContingencyTables.GridBoundary.denseRandomBitBudget