OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperLocalProposal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The small-chain proposal through the explicit local neighbor list

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.localNeighborList_codes line 20
  2. def OAI.ContingencyTables.SmallGraphProfiles.localBitProposal line 28

    Source documentation

    Binary lookup in the polynomial-length local list.

    def localBitProposal (x : PaperStates r c) (bits : Fin s → Bool) : Option (PaperStates r c) :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates

  3. theorem OAI.ContingencyTables.SmallGraphProfiles.localBitProposal_law line 33

    Source documentation

    The arithmetic enumeration implements exactly the proposal law used in the accepted-chain and mixing proofs.

    theorem localBitProposal_law (x : PaperStates r c) :
    mapLaw (uniformLaw (α := Fin s → Bool)) (localBitProposal r c x)=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.localBitProposal