OAI/Combinatorics/ContingencyTables/Transport/FiniteExchangeDegree.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A literal finite list of all unit-exchange neighbors

  1. def OAI.ContingencyTables.IntegerWeightedTransport.exchangeTarget line 15

    Source documentation

    The ordered pair records the coordinate raised and the coordinate lowered.

    def exchangeTarget (X : C → ℕ) (i j : C) : C → ℕ := fun a =>
…
  2. lemma OAI.ContingencyTables.IntegerWeightedTransport.adjacent_eq_exchangeTarget line 18
  3. def OAI.ContingencyTables.IntegerWeightedTransport.exchangeCandidates line 33
  4. lemma OAI.ContingencyTables.IntegerWeightedTransport.adjacent_mem_candidates line 36
  5. theorem OAI.ContingencyTables.IntegerWeightedTransport.exchangeCandidates_card_le line 41