OAI/Combinatorics/ContingencyTables/Transport/BoundedCellShift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A literal one-cell lower-bound reduction

Requiring the selected entry to be at least t is equivalent to subtracting t from that entry, its incident margins and its capacity. The three guards are retained explicitly, including for zero margins and structural zeros.

  1. def OAI.ContingencyTables.BoundedCellShift.margin line 19
  2. def OAI.ContingencyTables.BoundedCellShift.lower line 22
  3. def OAI.ContingencyTables.BoundedCellShift.raise line 26
  4. lemma OAI.ContingencyTables.BoundedCellShift.lower_raise line 30
  5. lemma OAI.ContingencyTables.BoundedCellShift.raise_lower line 35
  6. lemma OAI.ContingencyTables.BoundedCellShift.raise_row_sum line 43
  7. lemma OAI.ContingencyTables.BoundedCellShift.raise_column_sum line 51
  8. lemma OAI.ContingencyTables.BoundedCellShift.lower_margins line 59
  9. lemma OAI.ContingencyTables.BoundedCellShift.raise_margins line 88
  10. lemma OAI.ContingencyTables.BoundedCellShift.lower_bounds line 107
  11. lemma OAI.ContingencyTables.BoundedCellShift.raise_bounds line 116
  12. theorem OAI.ContingencyTables.BoundedCellShift.feasible_lower_iff line 129