OAI/Combinatorics/ContingencyTables/Machines/CanonicalInitialEncoding.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Canonical paired-label order for the initial binary program

The order is the explicit list of cells, then their copies, then the two sides of each pair. The code is obtained directly from the sampled Boolean rows, so no enumeration of the set-valued state space occurs.

  1. def OAI.ContingencyTables.CanonicalInitialEncoding.pairValue line 21
  2. def OAI.ContingencyTables.CanonicalInitialEncoding.pairValueRealizer line 23
  3. theorem OAI.ContingencyTables.CanonicalInitialEncoding.polynomial_pairValue line 27
  4. def OAI.ContingencyTables.CanonicalInitialEncoding.pairedCode line 34
  5. def OAI.ContingencyTables.CanonicalInitialEncoding.pairedCodeRealizer line 36
  6. theorem OAI.ContingencyTables.CanonicalInitialEncoding.polynomial_pairedCode line 38
  7. def OAI.ContingencyTables.CanonicalInitialEncoding.initialCode line 41
  8. def OAI.ContingencyTables.CanonicalInitialEncoding.initialCodeRealizer line 43
  9. theorem OAI.ContingencyTables.CanonicalInitialEncoding.polynomial_initialCode line 46
  10. def OAI.ContingencyTables.CanonicalInitialEncoding.copyOrder line 52
  11. def OAI.ContingencyTables.CanonicalInitialEncoding.pairOrder line 54
  12. lemma OAI.ContingencyTables.CanonicalInitialEncoding.copyOrder_nodup line 56
  13. lemma OAI.ContingencyTables.CanonicalInitialEncoding.copyOrder_mem line 59
  14. lemma OAI.ContingencyTables.CanonicalInitialEncoding.pairOrder_nodup line 63
  15. lemma OAI.ContingencyTables.CanonicalInitialEncoding.pairOrder_mem line 66
  16. def OAI.ContingencyTables.CanonicalInitialEncoding.coordinateEquiv line 71
  17. lemma OAI.ContingencyTables.CanonicalInitialEncoding.coordinateOrder line 74
  18. lemma OAI.ContingencyTables.CanonicalInitialEncoding.encodeSet_eq_map line 78
  19. lemma OAI.ContingencyTables.CanonicalInitialEncoding.pairedCode_eq_map line 85
  20. theorem OAI.ContingencyTables.CanonicalInitialEncoding.pairedCode_encode line 100

    Source documentation

    The explicit paired list order gives the same encoded set as the semantic local choices, including cells of capacity zero.

    theorem pairedCode_encode (v : ∀ i,Fin (b i) → Bool) :
    pairedCode (List.ofFn (fun i => List.ofFn (v i)))=
      CompanionArithmeticProposal.encodeSet (coordinateEquiv b)
        (encode b (fun i => subsetEquiv (b i) (v i))) := by
…

    Mentions: OAI.ContingencyTables.CanonicalInitialEncoding.pairedCode, OAI.ContingencyTables.CompanionArithmeticProposal.encodeSet, OAI.ContingencyTables.CanonicalInitialEncoding.coordinateEquiv

  21. theorem OAI.ContingencyTables.CanonicalInitialEncoding.initialCode_ofFn line 107