OAI/Combinatorics/ContingencyTables/Machines/InitialDrawReindex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact invariance of the finite initializer under computed cell order

  1. def OAI.ContingencyTables.InitialFactorialBits.finiteChoiceLaw line 16
  2. theorem OAI.ContingencyTables.InitialFactorialBits.transversalDraw_law line 27

    Source documentation

    Reordering the independent cell words changes no finite initializer law, including its finite-precision bias.

    theorem transversalDraw_law (b : C → ℕ) (e : C ≃ Fin q) (B : ℕ) :
    mapLaw (uniformLaw (α := Fin (bitCount (fun i => b (e.symm i)) B) → Bool))
…

    Mentions: OAI.ContingencyTables.InitialFactorialBits.bitCount

  3. theorem OAI.ContingencyTables.CompanionComputedInitial.initialDraw_law line 63
  4. theorem OAI.ContingencyTables.CompanionComputedInitial.initialProgram_sameLaw line 83