OAI/Combinatorics/ContingencyTables/Counting/CompanionStateMultiplierProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Reading the multiplier of an actual encoded chain state

The at most quadratic list of labelled defect types is searched using the proved occupancy test. Uniqueness of defect labels identifies the selected matrix entry with the mathematical chain multiplier.

  1. def OAI.ContingencyTables.CompanionStateMultiplierProgram.coordinates line 17
  2. def OAI.ContingencyTables.CompanionStateMultiplierProgram.coordinatesRealizer line 18
  3. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.polynomial_coordinates line 19
  4. def OAI.ContingencyTables.CompanionStateMultiplierProgram.candidates line 22
  5. def OAI.ContingencyTables.CompanionStateMultiplierProgram.candidatesRealizer line 23
  6. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.polynomial_candidates line 25
  7. def OAI.ContingencyTables.CompanionStateMultiplierProgram.found line 28
  8. def OAI.ContingencyTables.CompanionStateMultiplierProgram.foundRealizer line 30
  9. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.polynomial_found line 32
  10. abbrev OAI.ContingencyTables.CompanionStateMultiplierProgram.Input line 36
  11. def OAI.ContingencyTables.CompanionStateMultiplierProgram.noDefect line 38
  12. def OAI.ContingencyTables.CompanionStateMultiplierProgram.noDefectRealizer line 39
  13. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.polynomial_noDefect line 40
  14. def OAI.ContingencyTables.CompanionStateMultiplierProgram.readDefect line 43
  15. def OAI.ContingencyTables.CompanionStateMultiplierProgram.readDefectRealizer line 44
  16. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.polynomial_readDefect line 48
  17. def OAI.ContingencyTables.CompanionStateMultiplierProgram.output line 54
  18. def OAI.ContingencyTables.CompanionStateMultiplierProgram.outputRealizer line 55
  19. theorem OAI.ContingencyTables.CompanionStateMultiplierProgram.polynomial_output line 56
  20. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.candidates_mem line 66
  21. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.found_mem line 73
  22. lemma OAI.ContingencyTables.CompanionStateMultiplierProgram.found_exists line 85
  23. theorem OAI.ContingencyTables.CompanionStateMultiplierProgram.output_code line 102