OAI/Combinatorics/ContingencyTables/Counting/CompanionOrderedProposal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The companion proposal with a specified coordinate order

The coordinate scan and its paired-state validator work with the same explicit order used by the initializer. Its dyadic proposal law is independent of this order, including unused proposal words.

  1. def OAI.ContingencyTables.CompanionOrderedProposal.orderedNeighbors line 23
  2. lemma OAI.ContingencyTables.CompanionOrderedProposal.mem_orderedNeighbors line 26
  3. lemma OAI.ContingencyTables.CompanionOrderedProposal.orderedNeighbors_nodup line 30
  4. lemma OAI.ContingencyTables.CompanionOrderedProposal.orderedNeighbors_length line 33
  5. def OAI.ContingencyTables.CompanionOrderedProposal.orderedProposal line 43
  6. lemma OAI.ContingencyTables.CompanionOrderedProposal.orderedProposal_mass line 47
  7. theorem OAI.ContingencyTables.CompanionOrderedProposal.orderedProposal_law line 56

    Source documentation

    Every complete coordinate order has the analysed proposal law.

    theorem orderedProposal_law (e : (Labels A×Bool) ≃ Fin m) (S : State A) :
    mapLaw (uniformLaw (α := Fin (proposalBits A) → Bool)) (orderedProposal A e S)=
…

    Mentions: OAI.ContingencyTables.CompanionOrderedProposal.orderedProposal

  8. def OAI.ContingencyTables.CompanionOrderedProposal.orderedCatalog line 77
  9. lemma OAI.ContingencyTables.CompanionOrderedProposal.pairedStateTest_ordered line 80
  10. lemma OAI.ContingencyTables.CompanionOrderedProposal.validExchanges_ordered line 92
  11. theorem OAI.ContingencyTables.CompanionOrderedProposal.codeProposal_ordered line 114

    Source documentation

    The polynomial list program returns exactly the encoded state drawn by the ordered proposal; no enumeration of all chain states is needed.

    theorem codeProposal_ordered (g : Fin p ≃ Labels A) (e : (Labels A×Bool) ≃ Fin m)
    (S : State A) (bits : Fin (proposalBits A) → Bool) :
    codeProposal ((orderedCatalog A g e,encodeSet e S.val),List.ofFn bits)=
      (orderedProposal A e S bits).map (fun T => encodeSet e T.val) := by
…

    Mentions: OAI.ContingencyTables.CompanionOrderedProposal.orderedCatalog, OAI.ContingencyTables.CompanionOrderedProposal.orderedProposal