OAI/Combinatorics/ContingencyTables/Dense/GridIndexProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Binary indexing into the explicitly enumerated grid

  1. abbrev OAI.ContingencyTables.DensePrograms.GridIndexData line 12
  2. def OAI.ContingencyTables.DensePrograms.gridIndexPowerInput line 14
  3. def OAI.ContingencyTables.DensePrograms.gridIndexPowerInputRealizer line 17
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridIndexPowerInput line 21
  5. def OAI.ContingencyTables.DensePrograms.gridIndexTerm line 27
  6. def OAI.ContingencyTables.DensePrograms.gridIndexTermRealizer line 30
  7. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridIndexTerm line 37
  8. def OAI.ContingencyTables.DensePrograms.gridIndexIndices line 46
  9. def OAI.ContingencyTables.DensePrograms.gridIndexIndicesRealizer line 48
  10. lemma OAI.ContingencyTables.DensePrograms.polynomial_gridIndexIndices line 51
  11. def OAI.ContingencyTables.DensePrograms.gridIndex line 58
  12. def OAI.ContingencyTables.DensePrograms.gridIndexRealizer line 61
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_gridIndex line 67

    Source documentation

    Index computation is polynomial in the binary grid coordinates and base; the exponent loops are bounded by the coordinate list length.

    theorem polynomial_gridIndex : PolynomialTime gridIndexRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.gridIndexRealizer

  14. lemma OAI.ContingencyTables.DensePrograms.range_sum line 72
  15. lemma OAI.ContingencyTables.DensePrograms.gridIndex_ofFn line 80
  16. theorem OAI.ContingencyTables.DensePrograms.gridIndex_code line 92

    Source documentation

    The computed integer is exactly the position used by the state list.

    theorem gridIndex_code {q K : ℕ} (a : Grid (I := Fin q) K) :
…