OAI/Combinatorics/ContingencyTables/Machines/FixedCardinalityFold.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A polynomial sequential list program for the subset draw

The accumulator retains the remaining population and requested size, and records one inclusion bit per input word. Both counters decrease; only the output list grows. The final program reverses that list once.

  1. abbrev OAI.ContingencyTables.FixedCardinalityProgram.DrawState line 16
  2. def OAI.ContingencyTables.FixedCardinalityProgram.advance line 18
  3. def OAI.ContingencyTables.FixedCardinalityProgram.advanceRealizer line 22
  4. theorem OAI.ContingencyTables.FixedCardinalityProgram.polynomial_advance line 34
  5. lemma OAI.ContingencyTables.FixedCardinalityProgram.advance_bounds line 55
  6. lemma OAI.ContingencyTables.FixedCardinalityProgram.fold_bounds line 68
  7. def OAI.ContingencyTables.FixedCardinalityProgram.drawWords line 80
  8. def OAI.ContingencyTables.FixedCardinalityProgram.prepareWords line 83
  9. def OAI.ContingencyTables.FixedCardinalityProgram.prepareWordsRealizer line 85
  10. def OAI.ContingencyTables.FixedCardinalityProgram.runWords line 87
  11. def OAI.ContingencyTables.FixedCardinalityProgram.runWordsRealizer line 90
  12. def OAI.ContingencyTables.FixedCardinalityProgram.outputRealizer line 92
  13. def OAI.ContingencyTables.FixedCardinalityProgram.drawWordsRealizer line 94
  14. theorem OAI.ContingencyTables.FixedCardinalityProgram.polynomial_drawWords line 98
  15. def OAI.ContingencyTables.FixedCardinalityProgram.sampleWords line 134
  16. lemma OAI.ContingencyTables.FixedCardinalityProgram.fold_output line 140
  17. lemma OAI.ContingencyTables.FixedCardinalityProgram.drawWords_eq line 153
  18. theorem OAI.ContingencyTables.FixedCardinalityProgram.sampleWords_ofFn line 161
  19. theorem OAI.ContingencyTables.FixedCardinalityProgram.drawWords_ofFn line 176

    Source documentation

    The polynomial list program has exactly the proved sequential finite-word semantics, including empty populations.

    theorem drawWords_ofFn (B n k : ℕ) (words : Fin n → Fin B → Bool) :
    drawWords ((n,k),List.ofFn (fun i => List.ofFn (words i)))=
      List.ofFn (FixedCardinalityBits.draw B n k words) := by
…

    Mentions: OAI.ContingencyTables.FixedCardinalityProgram.drawWords, OAI.ContingencyTables.FixedCardinalityBits.draw