OAI/Combinatorics/ContingencyTables/Machines/InitialChoiceProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Polynomial independent-cell initialization program

The capacities are a supplied list. A polynomial index scan extracts each disjoint variable-width word block and runs the local subset program. The resulting rows are exactly the independent cell choices in the initial finite-word law.

  1. def OAI.ContingencyTables.InitialChoiceProgram.cellWidth line 20
  2. def OAI.ContingencyTables.InitialChoiceProgram.cellWidthRealizer line 22
  3. theorem OAI.ContingencyTables.InitialChoiceProgram.polynomial_cellWidth line 25
  4. def OAI.ContingencyTables.InitialChoiceProgram.widths line 30
  5. def OAI.ContingencyTables.InitialChoiceProgram.widthsRealizer line 32
  6. theorem OAI.ContingencyTables.InitialChoiceProgram.polynomial_widths line 35
  7. abbrev OAI.ContingencyTables.InitialChoiceProgram.Input line 39
  8. def OAI.ContingencyTables.InitialChoiceProgram.cellCode line 41
  9. def OAI.ContingencyTables.InitialChoiceProgram.cellCodeRealizer line 45
  10. theorem OAI.ContingencyTables.InitialChoiceProgram.polynomial_cellCode line 56
  11. def OAI.ContingencyTables.InitialChoiceProgram.indices line 74
  12. def OAI.ContingencyTables.InitialChoiceProgram.indicesRealizer line 76
  13. theorem OAI.ContingencyTables.InitialChoiceProgram.polynomial_indices line 79
  14. def OAI.ContingencyTables.InitialChoiceProgram.choiceCode line 86
  15. def OAI.ContingencyTables.InitialChoiceProgram.choiceCodeRealizer line 88
  16. theorem OAI.ContingencyTables.InitialChoiceProgram.polynomial_choiceCode line 91
  17. lemma OAI.ContingencyTables.InitialChoiceProgram.widths_ofFn line 99
  18. theorem OAI.ContingencyTables.InitialChoiceProgram.cellCode_ofFn line 105
  19. theorem OAI.ContingencyTables.InitialChoiceProgram.choiceCode_ofFn line 118

    Source documentation

    The executable product of cell programs gives exactly the Boolean rows whose support is the initial independent choice vector.

    theorem choiceCode_ofFn {q : ℕ} (b : Fin q → ℕ) (B : ℕ) (hB : 0<B)
    (bits : Fin (bitCount b B) → Bool) :
    choiceCode ((List.ofFn b,B),List.ofFn bits)=
      List.ofFn (fun i => List.ofFn (vectorDraw B (b i) (wordEquiv b B bits i))) := by
…

    Mentions: OAI.ContingencyTables.InitialChoiceProgram.choiceCode