OAI/Combinatorics/ContingencyTables/Machines/FixedCardinalityFlat.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A flat-word program for a local initial subset

The first B bits select the size. The remaining word is partitioned into B-bit inclusion rows, so the input list bounds the number of loop iterations even on malformed inputs.

  1. abbrev OAI.ContingencyTables.FixedCardinalityProgram.SubsetInput line 18
  2. def OAI.ContingencyTables.FixedCardinalityProgram.subsetCode line 20
  3. def OAI.ContingencyTables.FixedCardinalityProgram.subsetCodeRealizer line 24
  4. theorem OAI.ContingencyTables.FixedCardinalityProgram.polynomial_subsetCode line 33
  5. lemma OAI.ContingencyTables.FixedCardinalityProgram.splitWord_append line 53
  6. lemma OAI.ContingencyTables.FixedCardinalityProgram.splitWord_take line 68
  7. lemma OAI.ContingencyTables.FixedCardinalityProgram.splitWord_drop line 73
  8. theorem OAI.ContingencyTables.FixedCardinalityProgram.subsetCode_ofFn_raw line 78
  9. theorem OAI.ContingencyTables.FixedCardinalityProgram.subsetCode_ofFn line 89

    Source documentation

    Every local subset output bit agrees with the finite-word draw with the sequential subset law.

    theorem subsetCode_ofFn (B n : ℕ) (hB : 0<B)
    (bits : Fin (drawBits B n) → Bool) :
    subsetCode ((n,B),List.ofFn bits)=List.ofFn (vectorDraw B n bits) :=
…

    Mentions: OAI.ContingencyTables.FixedCardinalityProgram.subsetCode