OAI/Combinatorics/ContingencyTables/Transport/ComputedTableTightening.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact table bijection for the computed attained endpoints

The endpoint hypotheses of the translation lemma are discharged by the executed minimum and maximum searches, conditional only on EK1972.

  1. def OAI.ContingencyTables.ComputedTableTightening.lower line 19
  2. def OAI.ContingencyTables.ComputedTableTightening.upper line 22
  3. lemma OAI.ContingencyTables.ComputedTableTightening.lower_le line 32
  4. lemma OAI.ContingencyTables.ComputedTableTightening.le_upper line 38
  5. lemma OAI.ContingencyTables.ComputedTableTightening.lower_attained line 44
  6. lemma OAI.ContingencyTables.ComputedTableTightening.upper_attained line 49
  7. lemma OAI.ContingencyTables.ComputedTableTightening.upper_le_bound line 54
  8. lemma OAI.ContingencyTables.ComputedTableTightening.lower_le_upper line 58
  9. def OAI.ContingencyTables.ComputedTableTightening.newRows line 64
  10. def OAI.ContingencyTables.ComputedTableTightening.newColumns line 66
  11. def OAI.ContingencyTables.ComputedTableTightening.newBounds line 68
  12. def OAI.ContingencyTables.ComputedTableTightening.tighten line 70
  13. def OAI.ContingencyTables.ComputedTableTightening.restore line 77
  14. def OAI.ContingencyTables.ComputedTableTightening.tighteningEquiv line 85
  15. theorem OAI.ContingencyTables.ComputedTableTightening.count_eq line 99
  16. theorem OAI.ContingencyTables.ComputedTableTightening.attained_endpoints line 103