OAI/Combinatorics/ContingencyTables/Counting/CountingPreparedState.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Constructing the immutable rooted state from the public bounded input

  1. abbrev OAI.ContingencyTables.CountingPreparedState.Input line 10
  2. def OAI.ContingencyTables.CountingPreparedState.catalog line 12
  3. def OAI.ContingencyTables.CountingPreparedState.catalogRealizer line 13
  4. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_catalog line 14
  5. def OAI.ContingencyTables.CountingPreparedState.baseline line 16
  6. def OAI.ContingencyTables.CountingPreparedState.baselineRealizer line 17
  7. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_baseline line 20
  8. def OAI.ContingencyTables.CountingPreparedState.capacity line 23
  9. def OAI.ContingencyTables.CountingPreparedState.capacityRealizer line 24
  10. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_capacity line 25
  11. def OAI.ContingencyTables.CountingPreparedState.zeroMatrix line 27
  12. def OAI.ContingencyTables.CountingPreparedState.zeroMatrixRealizer line 28
  13. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_zeroMatrix line 30
  14. def OAI.ContingencyTables.CountingPreparedState.demand line 33
  15. def OAI.ContingencyTables.CountingPreparedState.demandRealizer line 35
  16. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_demand line 36
  17. def OAI.ContingencyTables.CountingPreparedState.parameters line 40
  18. def OAI.ContingencyTables.CountingPreparedState.parametersRealizer line 42
  19. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_parameters line 46
  20. def OAI.ContingencyTables.CountingPreparedState.zeroGrid line 51
  21. def OAI.ContingencyTables.CountingPreparedState.zeroGridRealizer line 52
  22. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_zeroGrid line 55
  23. def OAI.ContingencyTables.CountingPreparedState.state line 59
  24. def OAI.ContingencyTables.CountingPreparedState.stateRealizer line 61
  25. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_state line 63
  26. def OAI.ContingencyTables.CountingPreparedState.output line 67
  27. def OAI.ContingencyTables.CountingPreparedState.outputRealizer line 69
  28. lemma OAI.ContingencyTables.CountingPreparedState.polynomial_output line 70
  29. lemma OAI.ContingencyTables.CountingPreparedState.demand_data line 77
  30. def OAI.ContingencyTables.CountingPreparedState.start line 98
  31. lemma OAI.ContingencyTables.CountingPreparedState.state_data line 102
  32. lemma OAI.ContingencyTables.CountingPreparedState.start_transport line 134