OAI/Combinatorics/ContingencyTables/Dense/DenseEnumeratedMatrix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Computing every state of the dense transition table

  1. abbrev OAI.ContingencyTables.DensePrograms.EnumeratedMatrixInput line 12
  2. def OAI.ContingencyTables.DensePrograms.enumerationData line 14
  3. def OAI.ContingencyTables.DensePrograms.enumerationDataRealizer line 17
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_enumerationData line 23
  5. def OAI.ContingencyTables.DensePrograms.enumeratedMatrixInput line 33
  6. def OAI.ContingencyTables.DensePrograms.enumeratedMatrixInputRealizer line 36
  7. def OAI.ContingencyTables.DensePrograms.enumerationMeasure line 39
  8. lemma OAI.ContingencyTables.DensePrograms.work_enumeratedMatrixInput line 42
  9. def OAI.ContingencyTables.DensePrograms.enumeratedMatrix line 62
  10. def OAI.ContingencyTables.DensePrograms.enumeratedMatrixRealizer line 65
  11. theorem OAI.ContingencyTables.DensePrograms.work_enumeratedMatrix line 70

    Source documentation

    All states are generated from the dimension marker and grid size. The work is polynomial in their count and the supplied binary data.

    theorem work_enumeratedMatrix : WorkBound enumeratedMatrixRealizer enumerationMeasure :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.enumeratedMatrixRealizer, OAI.ContingencyTables.DensePrograms.enumerationMeasure

  12. theorem OAI.ContingencyTables.DensePrograms.enumeratedMatrix_actual line 73