OAI/Combinatorics/ContingencyTables/Sampling/SmallProfileCode.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.profileCode line 15
2. def OAI.ContingencyTables.SmallGraphProfiles.profileOfCode line 18
3. lemma OAI.ContingencyTables.SmallGraphProfiles.profileOfCode_code line 21
4. theorem OAI.ContingencyTables.SmallGraphProfiles.profileCode_injective line 30
5. lemma OAI.ContingencyTables.SmallGraphProfiles.ofFn_getD line 35
6. lemma OAI.ContingencyTables.SmallGraphProfiles.profileCode_ofCode line 43
7. def OAI.ContingencyTables.SmallGraphProfiles.codeCheckData line 51
8. theorem OAI.ContingencyTables.SmallGraphProfiles.profileTest_code_iff line 56

   Source documentation

   For arbitrary input lists, the Boolean program succeeds exactly when those lists encode an actual positive-completion state.

   theorem profileTest_code_iff (r : Fin m → ℕ) (c : Fin n → ℕ)
       (htotal : (∑ i,r i)=∑ j,c j) (e : Fin q ≃ Cells (paperSmall r c))
       (v : List ℕ×List ℕ) :
       profileTest (codeCheckData (cellCatalog (paperSmall r c) e) (List.ofFn r) (List.ofFn c)
         ((dimensionAllowance (I := Fin m) (J := Fin n))^20) v)=true ↔
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.codeCheckData, OAI.ContingencyTables.SmallGraphProfiles.cellCatalog