OAI/Combinatorics/ContingencyTables/Dense/DenseMatrixProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Polynomial assembly of the dense count matrix in column order

  1. abbrev OAI.ContingencyTables.DensePrograms.CountMatrixContext line 12
  2. abbrev OAI.ContingencyTables.DensePrograms.CountMatrixData line 13
  3. def OAI.ContingencyTables.DensePrograms.countMatrixEntryInput line 15
  4. def OAI.ContingencyTables.DensePrograms.countMatrixEntryInputRealizer line 18
  5. lemma OAI.ContingencyTables.DensePrograms.polynomial_countMatrixEntryInput line 28
  6. def OAI.ContingencyTables.DensePrograms.countMatrixEntry line 42
  7. def OAI.ContingencyTables.DensePrograms.countMatrixEntryRealizer line 45
  8. lemma OAI.ContingencyTables.DensePrograms.polynomial_countMatrixEntry line 48
  9. def OAI.ContingencyTables.DensePrograms.countColumn line 51
  10. def OAI.ContingencyTables.DensePrograms.countColumnRealizer line 54
  11. lemma OAI.ContingencyTables.DensePrograms.polynomial_countColumn line 57
  12. def OAI.ContingencyTables.DensePrograms.countMatrix line 62
  13. def OAI.ContingencyTables.DensePrograms.countMatrixRealizer line 65
  14. theorem OAI.ContingencyTables.DensePrograms.polynomial_countMatrix line 70

    Source documentation

    Preparation explicitly contains all states and one unary acceptance allowance. Matrix construction is polynomial in precisely that data.

    theorem polynomial_countMatrix : PolynomialTime countMatrixRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.countMatrixRealizer

  15. lemma OAI.ContingencyTables.DensePrograms.countMatrix_actual line 74