OAI/Combinatorics/ContingencyTables/Sampling/ProfileExchangeProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ProfilePrograms.ExchangeInput line 13
2. def OAI.ContingencyTables.ProfilePrograms.exchangeEntry line 15
3. def OAI.ContingencyTables.ProfilePrograms.exchangeEntryRealizer line 18
4. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_exchangeEntry line 31
5. def OAI.ContingencyTables.ProfilePrograms.listExchange line 52
6. def OAI.ContingencyTables.ProfilePrograms.listExchangeRealizer line 55
7. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_listExchange line 61

   Source documentation

   Its loop traverses the input profile once, even if the supplied coordinate indices are much larger than its length.

   theorem polynomial_listExchange : PolynomialTime listExchangeRealizer := by
   …

   Mentions: OAI.ContingencyTables.ProfilePrograms.listExchangeRealizer

8. lemma OAI.ContingencyTables.ProfilePrograms.listExchange_length line 71
9. theorem OAI.ContingencyTables.ProfilePrograms.listExchange_ofFn line 76

   Source documentation

   The binary list program implements the exact coordinate update used by the physical graph, with no bounded-integer overflow.

   theorem listExchange_ofFn {n : ℕ} (v : Fin n → ℕ) (i j : Fin n) :
       listExchange (List.ofFn v,(i.val,j.val))=
         List.ofFn (IntegerWeightedTransport.exchangeTarget v i j) := by
   …

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