OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperBooleanProposal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite Boolean realization of the small graph proposal law

  1. abbrev OAI.ContingencyTables.SmallGraphProfiles.smallProposalBits line 20
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.smallProposal_codes line 22
  3. def OAI.ContingencyTables.SmallGraphProfiles.smallBitProposal line 32
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.smallBitProposal_law_decidableEq line 38

    Source documentation

    The law is independent of the equality decision used by a consumer.

    theorem smallBitProposal_law_decidableEq (d₀ : DecidableEq (Option (PaperStates r c)))
    (x : PaperStates r c) :
    @mapLaw (Fin (smallProposalBits (I := I) (J := J)) → Bool)
…

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

  5. theorem OAI.ContingencyTables.SmallGraphProfiles.smallBitProposal_law line 56

    Source documentation

    The coding assigns one bit word to each distinct neighbor and uses all remaining words for the holding proposal. Enumeration cost is separate.

    theorem smallBitProposal_law (x : PaperStates r c) :
    mapLaw (uniformLaw (α := Fin (smallProposalBits (I := I) (J := J)) → Bool))
…

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