OAI/Combinatorics/ContingencyTables/Dense/DenseCompletionTest.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A polynomial exact acceptance test for a free integer matrix

  1. def OAI.ContingencyTables.DensePrograms.completionNonnegative line 10
  2. def OAI.ContingencyTables.DensePrograms.completionNonnegativeRealizer line 13
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_completionNonnegative line 16
  4. def OAI.ContingencyTables.DensePrograms.completionValid line 20
  5. def OAI.ContingencyTables.DensePrograms.completionValidRealizer line 23
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_completionValid line 29
  7. theorem OAI.ContingencyTables.DensePrograms.completionNonnegative_code line 34
  8. theorem OAI.ContingencyTables.DensePrograms.completionValid_code line 45