OAI/Combinatorics/ContingencyTables/Dense/DenseExponentListProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Computing all dense exponent components and their maximum

  1. def OAI.ContingencyTables.DensePrograms.listMaximum line 12
  2. def OAI.ContingencyTables.DensePrograms.listMaximumRealizer line 14
  3. lemma OAI.ContingencyTables.DensePrograms.polynomial_maximum line 16
  4. lemma OAI.ContingencyTables.DensePrograms.foldMaximum_size line 20
  5. theorem OAI.ContingencyTables.DensePrograms.polynomial_listMaximum line 33
  6. lemma OAI.ContingencyTables.DensePrograms.listMaximum_le line 48
  7. lemma OAI.ContingencyTables.DensePrograms.le_listMaximum_default line 66
  8. lemma OAI.ContingencyTables.DensePrograms.le_listMaximum_member line 69
  9. abbrev OAI.ContingencyTables.DensePrograms.ExponentData line 72
  10. def OAI.ContingencyTables.DensePrograms.exponentCellData line 74
  11. def OAI.ContingencyTables.DensePrograms.exponentCellDataRealizer line 78
  12. theorem OAI.ContingencyTables.DensePrograms.polynomial_exponentCellData line 90
  13. def OAI.ContingencyTables.DensePrograms.exponentCell line 110
  14. def OAI.ContingencyTables.DensePrograms.exponentCellRealizer line 112
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_exponentCell line 115
  16. def OAI.ContingencyTables.DensePrograms.exponentCells line 118
  17. def OAI.ContingencyTables.DensePrograms.exponentCellsRealizer line 120
  18. theorem OAI.ContingencyTables.DensePrograms.polynomial_exponentCells line 123
  19. def OAI.ContingencyTables.DensePrograms.exponentValues line 126
  20. def OAI.ContingencyTables.DensePrograms.exponentValuesRealizer line 129
  21. theorem OAI.ContingencyTables.DensePrograms.polynomial_exponentValues line 132
  22. def OAI.ContingencyTables.DensePrograms.fullExponent line 136
  23. def OAI.ContingencyTables.DensePrograms.fullExponentRealizer line 138
  24. theorem OAI.ContingencyTables.DensePrograms.polynomial_fullExponent line 142

    Source documentation

    The exponent evaluation traverses only the supplied matrix dimensions.

    theorem polynomial_fullExponent : PolynomialTime fullExponentRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.fullExponentRealizer