OAI/Combinatorics/ContingencyTables/Transport/IntegerSliceRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restricting fixed prefix coordinates

A context is fixed before the signed transport starts. Its coordinates are removed from the transport index set, so leaf cliques cannot move a hole into that prefix. The remaining removal form is a principal block.

  1. lemma OAI.ContingencyTables.IntegerWeightedTransport.removeOne_fixed line 20
  2. lemma OAI.ContingencyTables.IntegerWeightedTransport.removeTwo_fixed line 26
  3. lemma OAI.ContingencyTables.IntegerWeightedTransport.removalMatrix_fixed line 31
  4. lemma OAI.ContingencyTables.IntegerWeightedTransport.removalSignature_fixed line 41
  5. theorem OAI.ContingencyTables.IntegerWeightedTransport.positiveSlice_fixed line 52
  6. theorem OAI.ContingencyTables.IntegerWeightedTransport.removalSlice_fixed line 64