OAI/Combinatorics/ContingencyTables/Dense/DenseNormalizeProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Moving maximal margins into the distinguished positions

  1. def OAI.ContingencyTables.DensePrograms.swapMargins line 10
  2. def OAI.ContingencyTables.DensePrograms.swapMarginsRealizer line 13
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapMargins line 17
  4. def OAI.ContingencyTables.DensePrograms.swapFlatData line 24
  5. def OAI.ContingencyTables.DensePrograms.swapFlatDataRealizer line 27
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapFlatData line 32
  7. def OAI.ContingencyTables.DensePrograms.permuteDrawData line 41
  8. def OAI.ContingencyTables.DensePrograms.permuteDrawDataRealizer line 44
  9. theorem OAI.ContingencyTables.DensePrograms.polynomial_permuteDrawData line 51
  10. def OAI.ContingencyTables.DensePrograms.marginIndices line 63
  11. def OAI.ContingencyTables.DensePrograms.marginIndicesRealizer line 64
  12. theorem OAI.ContingencyTables.DensePrograms.polynomial_marginIndices line 67
  13. def OAI.ContingencyTables.DensePrograms.drawIndices line 71
  14. def OAI.ContingencyTables.DensePrograms.drawIndicesRealizer line 73
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_drawIndices line 78
  16. def OAI.ContingencyTables.DensePrograms.preparedDraw line 85
  17. def OAI.ContingencyTables.DensePrograms.preparedDrawRealizer line 88
  18. theorem OAI.ContingencyTables.DensePrograms.polynomial_preparedDraw line 91
  19. def OAI.ContingencyTables.DensePrograms.normalizedDraw line 95
  20. def OAI.ContingencyTables.DensePrograms.normalizedDrawRealizer line 97
  21. theorem OAI.ContingencyTables.DensePrograms.polynomial_normalizedDraw line 100
  22. def OAI.ContingencyTables.DensePrograms.normalizedDenseCode line 103
  23. def OAI.ContingencyTables.DensePrograms.normalizedDenseCodeRealizer line 106
  24. theorem OAI.ContingencyTables.DensePrograms.polynomial_normalizedDenseCode line 111

    Source documentation

    Maximal-margin selection, forward permutation, the full dense draw, and the inverse permutation all have polynomial binary cost.

    theorem polynomial_normalizedDenseCode : PolynomialTime normalizedDenseCodeRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.normalizedDenseCodeRealizer