OAI/Combinatorics/ContingencyTables/Counting/CompanionInitialMatrixProgram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Executing the initial canonical multiplier matrix

  1. abbrev OAI.ContingencyTables.CompanionInitialMatrixProgram.Metadata line 12
  2. def OAI.ContingencyTables.CompanionInitialMatrixProgram.numerator line 14
  3. def OAI.ContingencyTables.CompanionInitialMatrixProgram.numeratorRealizer line 15
  4. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_numerator line 19
  5. def OAI.ContingencyTables.CompanionInitialMatrixProgram.denominator line 24
  6. def OAI.ContingencyTables.CompanionInitialMatrixProgram.denominatorRealizer line 25
  7. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_denominator line 29
  8. def OAI.ContingencyTables.CompanionInitialMatrixProgram.sameCell line 33
  9. def OAI.ContingencyTables.CompanionInitialMatrixProgram.sameCellRealizer line 34
  10. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_sameCell line 36
  11. def OAI.ContingencyTables.CompanionInitialMatrixProgram.entry line 40
  12. def OAI.ContingencyTables.CompanionInitialMatrixProgram.entryRealizer line 42
  13. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_entry line 45
  14. def OAI.ContingencyTables.CompanionInitialMatrixProgram.row line 50
  15. def OAI.ContingencyTables.CompanionInitialMatrixProgram.rowRealizer line 52
  16. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_row line 53
  17. def OAI.ContingencyTables.CompanionInitialMatrixProgram.matrix line 57
  18. def OAI.ContingencyTables.CompanionInitialMatrixProgram.matrixRealizer line 58
  19. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_matrix line 59
  20. def OAI.ContingencyTables.CompanionInitialMatrixProgram.output line 63
  21. def OAI.ContingencyTables.CompanionInitialMatrixProgram.outputRealizer line 65
  22. theorem OAI.ContingencyTables.CompanionInitialMatrixProgram.polynomial_output line 68
  23. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.entry_val line 71
  24. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.matrix_ofFn line 81
  25. def OAI.ContingencyTables.CompanionInitialMatrixProgram.metadataAt line 93
  26. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.metadata_code line 96
  27. theorem OAI.ContingencyTables.CompanionInitialMatrixProgram.output_code line 104
  28. def OAI.ContingencyTables.CompanionInitialMatrixProgram.initialEntries line 111
  29. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.pairLabels_cell line 114
  30. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.metadata_cell_iff line 119
  31. lemma OAI.ContingencyTables.CompanionInitialMatrixProgram.metadata_capacity line 131
  32. theorem OAI.ContingencyTables.CompanionInitialMatrixProgram.initialEntries_val line 138
  33. theorem OAI.ContingencyTables.CompanionInitialMatrixProgram.output_physical line 147