OAI/Combinatorics/ContingencyTables/Transport/IntegerExchangeArithmetic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic recognition of unit-exchange edges

  1. lemma OAI.ContingencyTables.IntegerWeightedTransport.exchangeTarget_adjacent line 12
  2. theorem OAI.ContingencyTables.IntegerWeightedTransport.adjacent_iff_arithmetic line 26

    Source documentation

    The test quantifies only over two coordinates, never over profiles.

    theorem adjacent_iff_arithmetic (X Y : C → ℕ) :
    IntegerExchangeAdjacent X Y ↔
      ∃ i j,i≠j ∧ 0<X j ∧ Y=exchangeTarget X i j := by
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.IntegerExchangeAdjacent, OAI.ContingencyTables.IntegerWeightedTransport.exchangeTarget