OAI/Combinatorics/ContingencyTables/Dense/DenseBooleanOffsets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Independent actual Boolean offset draws realize the bounded offset law

  1. abbrev OAI.ContingencyTables.GridBoundary.OffsetWords line 18
  2. def OAI.ContingencyTables.GridBoundary.drawOffsetWords line 21
  3. theorem OAI.ContingencyTables.GridBoundary.drawOffsetWordsLaw_eq line 28

    Source documentation

    Every coordinate uses its declared independent bounded Boolean word; the resulting offset vector has the bounded quotient-offset law.

    theorem drawOffsetWordsLaw_eq (e : I × J ≃ Fin q) (w : I × J → ℕ)
    [DecidableEq (Offset w)]
    (hw : ∀ p, 0 < w p) (h d : ℕ) :
    mapLaw (uniformLaw (α := OffsetWords e w h d)) (drawOffsetWords e w hw h d) =
…

    Mentions: OAI.ContingencyTables.GridBoundary.Offset, OAI.ContingencyTables.GridBoundary.OffsetWords, OAI.ContingencyTables.GridBoundary.drawOffsetWords