OAI/Combinatorics/ContingencyTables/Counting/CompanionArithmeticProposal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

An explicit coordinate-list proposal for the companion chain

Only ordered coordinates are enumerated. The arithmetic binary-profile program generates the possible exchanges, after which the actual chain state predicate removes disallowed states. A dyadic list index has exactly the same proposal law as the abstract injection.

  1. def OAI.ContingencyTables.CompanionArithmeticProposal.coordinateSet line 26
  2. def OAI.ContingencyTables.CompanionArithmeticProposal.physicalSet line 28
  3. lemma OAI.ContingencyTables.CompanionArithmeticProposal.physical_coordinate line 31
  4. lemma OAI.ContingencyTables.CompanionArithmeticProposal.coordinate_physical line 36
  5. lemma OAI.ContingencyTables.CompanionArithmeticProposal.adjacent_preimage line 41
  6. lemma OAI.ContingencyTables.CompanionArithmeticProposal.adjacent_coordinate_iff line 54
  7. def OAI.ContingencyTables.CompanionArithmeticProposal.encodeSet line 63
  8. def OAI.ContingencyTables.CompanionArithmeticProposal.decodeSet line 65
  9. lemma OAI.ContingencyTables.CompanionArithmeticProposal.decode_encode line 68
  10. lemma OAI.ContingencyTables.CompanionArithmeticProposal.encode_injective line 75
  11. lemma OAI.ContingencyTables.CompanionArithmeticProposal.encode_physical line 81
  12. lemma OAI.ContingencyTables.CompanionArithmeticProposal.decode_profile line 86
  13. theorem OAI.ContingencyTables.CompanionArithmeticProposal.mem_raw_codes line 91

    Source documentation

    The executable integer update enumerates exactly the set exchanges.

    theorem mem_raw_codes (S : Set Γ) (xs : List ℕ) :
    xs∈binaryExchanges (encodeSet e S) ↔
      ∃ T : Set Γ,ExchangeAdjacent S T ∧ xs=encodeSet e T := by
…

    Mentions: OAI.ContingencyTables.CompanionArithmeticProposal.encodeSet

  14. def OAI.ContingencyTables.CompanionArithmeticProposal.neighborSets line 107
  15. lemma OAI.ContingencyTables.CompanionArithmeticProposal.mem_neighborSets line 110
  16. lemma OAI.ContingencyTables.CompanionArithmeticProposal.neighborSets_nodup line 119
  17. def OAI.ContingencyTables.CompanionArithmeticProposal.neighborStates line 127

    Source documentation

    The state filter is applied after the quadratic coordinate scan.

    def neighborStates (gs : List (Γ×Γ)) (S : ChainIndex gs) : List (ChainIndex gs) :=
…
  18. lemma OAI.ContingencyTables.CompanionArithmeticProposal.stateFilter_eq_some line 131
  19. lemma OAI.ContingencyTables.CompanionArithmeticProposal.mem_neighborStates line 140
  20. lemma OAI.ContingencyTables.CompanionArithmeticProposal.neighborStates_nodup line 149
  21. def OAI.ContingencyTables.CompanionArithmeticProposal.coordinateEquiv line 161
  22. def OAI.ContingencyTables.CompanionArithmeticProposal.neighbors line 164
  23. theorem OAI.ContingencyTables.CompanionArithmeticProposal.mem_neighbors line 167
  24. theorem OAI.ContingencyTables.CompanionArithmeticProposal.neighbors_nodup line 171
  25. theorem OAI.ContingencyTables.CompanionArithmeticProposal.neighbors_length line 174
  26. def OAI.ContingencyTables.CompanionArithmeticProposal.proposal line 183

    Source documentation

    The selection stage is the actual binary list-index program.

    def proposal (A : Instance I J) (S : State A) (bits : Fin (proposalBits A) → Bool) : Option (State A) :=
…
  27. theorem OAI.ContingencyTables.CompanionArithmeticProposal.proposal_mass line 186
  28. theorem OAI.ContingencyTables.CompanionArithmeticProposal.proposal_law line 194

    Source documentation

    The explicit arithmetic enumeration changes no proposal probabilities, including the unused-code outcome.

    theorem proposal_law (A : Instance I J) (S : State A) :
    mapLaw (uniformLaw (α := Fin (proposalBits A) → Bool)) (proposal A S)=
…

    Mentions: OAI.ContingencyTables.CompanionArithmeticProposal.proposal