OAI/Combinatorics/ContingencyTables/Transport/BoundedTableComplement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Complementing a bounded table

The map X ↦ b-X transforms cell minima into maxima. All margin subtractions are justified by an actual feasible table.

  1. def OAI.ContingencyTables.BoundedTableComplement.complement line 17
  2. def OAI.ContingencyTables.BoundedTableComplement.rowTotal line 19
  3. def OAI.ContingencyTables.BoundedTableComplement.columnTotal line 20
  4. def OAI.ContingencyTables.BoundedTableComplement.rows line 22
  5. def OAI.ContingencyTables.BoundedTableComplement.columns line 23
  6. lemma OAI.ContingencyTables.BoundedTableComplement.complement_bounds line 25
  7. lemma OAI.ContingencyTables.BoundedTableComplement.complement_twice line 28
  8. lemma OAI.ContingencyTables.BoundedTableComplement.complement_margins line 33
  9. lemma OAI.ContingencyTables.BoundedTableComplement.row_total_ge line 56
  10. lemma OAI.ContingencyTables.BoundedTableComplement.column_total_ge line 62
  11. lemma OAI.ContingencyTables.BoundedTableComplement.margins_twice line 68
  12. lemma OAI.ContingencyTables.BoundedTableComplement.complement_reverse_margins line 77