OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperBooleanStep.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual small transition driven by one fixed Boolean word

  1. def OAI.ContingencyTables.SmallGraphProfiles.smallBitStep line 34
  2. theorem OAI.ContingencyTables.SmallGraphProfiles.smallBitStep_law line 40

    Source documentation

    The proposal and the completion consume disjoint fixed segments.

    theorem smallBitStep_law (x : PaperStates r c) :
    mapLaw (uniformLaw (α := Fin (s+f) → Bool))
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates