OAI/Combinatorics/ContingencyTables/Machines/PreparedOffsetCount.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Binary evaluation of the offset numerator product

  1. abbrev OAI.ContingencyTables.DensePrograms.PreparedOffsetData line 14

    Source documentation

    A shared bit allowance, widths, actual bit lengths and offsets.

    abbrev PreparedOffsetData := ((List Bool×List ℕ)×List ℕ)×List ℕ
  2. def OAI.ContingencyTables.DensePrograms.preparedOffsetInput line 16
  3. def OAI.ContingencyTables.DensePrograms.preparedOffsetInputRealizer line 21
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_preparedOffsetInput line 36
  5. def OAI.ContingencyTables.DensePrograms.preparedOffsetFactor line 54
  6. def OAI.ContingencyTables.DensePrograms.preparedOffsetFactorRealizer line 57
  7. lemma OAI.ContingencyTables.DensePrograms.polynomial_preparedOffsetFactor line 60
  8. def OAI.ContingencyTables.DensePrograms.preparedOffsetIndices line 63
  9. def OAI.ContingencyTables.DensePrograms.preparedOffsetIndicesRealizer line 65
  10. lemma OAI.ContingencyTables.DensePrograms.polynomial_preparedOffsetIndices line 68
  11. def OAI.ContingencyTables.DensePrograms.preparedOffsetProduct line 77
  12. def OAI.ContingencyTables.DensePrograms.preparedOffsetProductRealizer line 80
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_preparedOffsetProduct line 86

    Source documentation

    The product uses binary ceiling divisions and shared bounded powers. It is polynomial in its supplied bit allowance and integer data.

    theorem polynomial_preparedOffsetProduct : PolynomialTime preparedOffsetProductRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.preparedOffsetProductRealizer

  14. lemma OAI.ContingencyTables.DensePrograms.preparedOffsetFactor_ofFn line 91
  15. lemma OAI.ContingencyTables.DensePrograms.range_prod line 99
  16. theorem OAI.ContingencyTables.DensePrograms.preparedOffsetProduct_ofFn line 107