OAI/Combinatorics/ContingencyTables/Machines/BinaryExchangeProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Polynomial enumeration of exchanges of a binary profile

The program scans at most the square of the list length. It retains only an absent receiving coordinate and a present donating coordinate, so every retained natural-number update is again a binary profile.

  1. def OAI.ContingencyTables.ProfilePrograms.binaryExchangeTest line 17
  2. def OAI.ContingencyTables.ProfilePrograms.binaryExchangeTestRealizer line 20
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_binaryExchangeTest line 32
  4. def OAI.ContingencyTables.ProfilePrograms.binaryExchangeIndices line 46
  5. def OAI.ContingencyTables.ProfilePrograms.binaryExchangeIndicesRealizer line 49
  6. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_binaryExchangeIndices line 53
  7. theorem OAI.ContingencyTables.ProfilePrograms.mem_binaryExchangeIndices line 58
  8. lemma OAI.ContingencyTables.ProfilePrograms.cellPairs_nodup line 65
  9. theorem OAI.ContingencyTables.ProfilePrograms.binaryExchangeIndices_nodup line 76
  10. def OAI.ContingencyTables.ProfilePrograms.binaryExchanges line 79
  11. def OAI.ContingencyTables.ProfilePrograms.binaryExchangesRealizer line 82
  12. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_binaryExchanges line 85
  13. def OAI.ContingencyTables.ProfilePrograms.setProfile line 89
  14. lemma OAI.ContingencyTables.ProfilePrograms.setProfile_injective line 92
  15. theorem OAI.ContingencyTables.ProfilePrograms.exchange_setProfile line 100

    Source documentation

    On an absent/present coordinate pair, the natural update is exactly set removal followed by set insertion.

    theorem exchange_setProfile {n : ℕ} (S : Set (Fin n)) (i j : Fin n)
    (hi : i∉S) (hj : j∈S) :
    IntegerWeightedTransport.exchangeTarget (setProfile S) i j=
      setProfile (insert i (S\{j})) := by
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.exchangeTarget, OAI.ContingencyTables.ProfilePrograms.setProfile

  16. theorem OAI.ContingencyTables.ProfilePrograms.mem_binaryExchanges_setProfile line 117

    Source documentation

    Every program output is a genuine binary exchange, and all such exchanges are listed. No enumeration of the set of states is involved.

    theorem mem_binaryExchanges_setProfile {n : ℕ} (S : Set (Fin n)) (ys : List ℕ) :
    ys∈binaryExchanges (List.ofFn (setProfile S)) ↔
      ∃ i j : Fin n,i∉S ∧ j∈S ∧ ys=List.ofFn (setProfile (insert i (S\{j}))) := by
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.binaryExchanges, OAI.ContingencyTables.ProfilePrograms.setProfile

  17. lemma OAI.ContingencyTables.ProfilePrograms.getD_setProfile line 152
  18. lemma OAI.ContingencyTables.ProfilePrograms.binaryIndex_specs line 157
  19. theorem OAI.ContingencyTables.ProfilePrograms.binaryExchanges_nodup line 176

    Source documentation

    Distinct eligible coordinate pairs give distinct binary profiles.

    theorem binaryExchanges_nodup {n : ℕ} (S : Set (Fin n)) :
    (binaryExchanges (List.ofFn (setProfile S))).Nodup := by
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.binaryExchanges, OAI.ContingencyTables.ProfilePrograms.setProfile