OAI/Combinatorics/ContingencyTables/Sampling/ProfileExchangeCandidates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A polynomial binary program listing all coordinate exchanges

  1. def OAI.ContingencyTables.ProfilePrograms.profileIndices line 11
  2. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileIndices line 14
  3. def OAI.ContingencyTables.ProfilePrograms.exchangeRow line 19
  4. def OAI.ContingencyTables.ProfilePrograms.exchangeRowRealizer line 22
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_exchangeRow line 28
  6. def OAI.ContingencyTables.ProfilePrograms.allExchanges line 37
  7. def OAI.ContingencyTables.ProfilePrograms.allExchangesRealizer line 40
  8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_allExchanges line 43
  9. lemma OAI.ContingencyTables.ProfilePrograms.exchangeRow_length line 48
  10. theorem OAI.ContingencyTables.ProfilePrograms.allExchanges_length line 51
  11. theorem OAI.ContingencyTables.ProfilePrograms.mem_allExchanges_ofFn line 57

    Source documentation

    Every generated vector is an actual ordered-coordinate update, and every such update occurs. Duplicate profiles can be removed later.

    theorem mem_allExchanges_ofFn {n : ℕ} (v : Fin n → ℕ) (xs : List ℕ) :
    xs ∈ allExchanges (List.ofFn v) ↔
      ∃ i j : Fin n,xs=List.ofFn (IntegerWeightedTransport.exchangeTarget v i j) := by
…

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