OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperBooleanDraw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed Boolean words for the entire small walk and outer sampler

  1. def OAI.ContingencyTables.SmallGraphProfiles.flatSmallWalk line 32
  2. theorem OAI.ContingencyTables.SmallGraphProfiles.flatSmallWalk_law line 37
  3. def OAI.ContingencyTables.SmallGraphProfiles.smallJointDraw line 48
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.smallJointDraw_law line 56

    Source documentation

    The terminal completion uses fresh bits at the adaptively obtained state, with exactly the joint law used in the error proof.

    theorem smallJointDraw_law (x : PaperStates r c) (n : ℕ) :
    mapLaw (uniformLaw (α := Fin (n*(s+f)+f) → Bool))
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates

  5. def OAI.ContingencyTables.SmallGraphProfiles.finiteOuterDraw line 81
  6. theorem OAI.ContingencyTables.SmallGraphProfiles.finiteOuterDraw_law line 89

    Source documentation

    All trial words are independent and failed trials return the fixed feasible fallback. In particular, every bit word returns a feasible table.

    theorem finiteOuterDraw_law (x : PaperStates r c) (n J₀ : ℕ) (z₀ : Table r c) :
    mapLaw (uniformLaw (α := Fin (J₀*(n*(s+f)+f)) → Bool))
…

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