OAI/Combinatorics/ContingencyTables/Counting/CompanionInitialStoredProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The literal initial count and stored multiplier matrix

The integer count is the product of the free-cell ranges and the small-cell ranges. Both lists come from the executed forest and cell catalogs.

  1. abbrev OAI.ContingencyTables.CompanionInitialStoredProgram.Input line 15
  2. def OAI.ContingencyTables.CompanionInitialStoredProgram.rangeAt line 17
  3. def OAI.ContingencyTables.CompanionInitialStoredProgram.rangeAtRealizer line 18
  4. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.polynomial_rangeAt line 23
  5. def OAI.ContingencyTables.CompanionInitialStoredProgram.freeRanges line 28
  6. def OAI.ContingencyTables.CompanionInitialStoredProgram.freeRangesRealizer line 30
  7. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.polynomial_freeRanges line 36
  8. def OAI.ContingencyTables.CompanionInitialStoredProgram.freeProduct line 41
  9. def OAI.ContingencyTables.CompanionInitialStoredProgram.freeProductRealizer line 42
  10. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.polynomial_freeProduct line 44
  11. def OAI.ContingencyTables.CompanionInitialStoredProgram.smallProduct line 47
  12. def OAI.ContingencyTables.CompanionInitialStoredProgram.smallProductRealizer line 48
  13. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.polynomial_smallProduct line 49
  14. def OAI.ContingencyTables.CompanionInitialStoredProgram.total line 52
  15. def OAI.ContingencyTables.CompanionInitialStoredProgram.totalRealizer line 54
  16. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.polynomial_total line 60
  17. def OAI.ContingencyTables.CompanionInitialStoredProgram.output line 66
  18. def OAI.ContingencyTables.CompanionInitialStoredProgram.outputRealizer line 68
  19. theorem OAI.ContingencyTables.CompanionInitialStoredProgram.polynomial_output line 71
  20. def OAI.ContingencyTables.CompanionInitialStoredProgram.data line 81
  21. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.rangeAt_data line 84
  22. lemma OAI.ContingencyTables.CompanionInitialStoredProgram.freeRanges_data line 89
  23. theorem OAI.ContingencyTables.CompanionInitialStoredProgram.total_data line 104
  24. theorem OAI.ContingencyTables.CompanionInitialStoredProgram.output_matrix line 115