OAI/Combinatorics/ContingencyTables/Machines/BinIntervalProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Binary evaluation of a bin interval and its bounded quotient draw

The lower endpoint is computed as the negative floor of a negative rational. Thus the executed arithmetic uses natural quotient/remainder, without enumerating any of the integers in the interval.

  1. abbrev OAI.ContingencyTables.BinIntervalProgram.Input line 19

    Source documentation

    (number of bins, range size, bin index).

    abbrev Input := (ℕ×ℕ)×ℕ
  2. def OAI.ContingencyTables.BinIntervalProgram.negativeInput line 21
  3. def OAI.ContingencyTables.BinIntervalProgram.negativeInputRealizer line 23
  4. lemma OAI.ContingencyTables.BinIntervalProgram.polynomial_negativeInput line 28
  5. def OAI.ContingencyTables.BinIntervalProgram.endpoint line 34
  6. def OAI.ContingencyTables.BinIntervalProgram.endpointRealizer line 36
  7. theorem OAI.ContingencyTables.BinIntervalProgram.polynomial_endpoint line 43
  8. theorem OAI.ContingencyTables.BinIntervalProgram.endpoint_eq line 48
  9. def OAI.ContingencyTables.BinIntervalProgram.next line 58
  10. def OAI.ContingencyTables.BinIntervalProgram.nextRealizer line 59
  11. lemma OAI.ContingencyTables.BinIntervalProgram.polynomial_next line 60
  12. def OAI.ContingencyTables.BinIntervalProgram.intervalSize line 63
  13. def OAI.ContingencyTables.BinIntervalProgram.intervalSizeRealizer line 64
  14. theorem OAI.ContingencyTables.BinIntervalProgram.polynomial_intervalSize line 69
  15. theorem OAI.ContingencyTables.BinIntervalProgram.intervalSize_eq line 74
  16. def OAI.ContingencyTables.BinIntervalProgram.draw line 80
  17. def OAI.ContingencyTables.BinIntervalProgram.drawRealizer line 82
  18. theorem OAI.ContingencyTables.BinIntervalProgram.polynomial_draw line 92
  19. theorem OAI.ContingencyTables.BinIntervalProgram.draw_mem line 99
  20. theorem OAI.ContingencyTables.BinIntervalProgram.draw_ofFn line 108