OAI/Combinatorics/ContingencyTables/Machines/ScalarScheduleProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Fixed arithmetic circuits for the scalar counting schedules

These circuits only read a fixed finite list and perform binary addition and multiplication. Their syntax describes the fixed program, not a numeric loop selected by the input.

  1. inductive OAI.ContingencyTables.ScalarScheduleProgram.Expr line 16
  2. def OAI.ContingencyTables.ScalarScheduleProgram.Expr.eval line 22
  3. def OAI.ContingencyTables.ScalarScheduleProgram.Expr.realizer line 28
  4. lemma OAI.ContingencyTables.ScalarScheduleProgram.Expr.polynomial line 34
  5. def OAI.ContingencyTables.ScalarScheduleProgram.Expr.pow line 42
  6. lemma OAI.ContingencyTables.ScalarScheduleProgram.Expr.eval_pow line 46
  7. instance OAI.ContingencyTables.ScalarScheduleProgram.(instance at line 53) line 53
  8. instance OAI.ContingencyTables.ScalarScheduleProgram.(instance at line 54) line 54
  9. instance OAI.ContingencyTables.ScalarScheduleProgram.(instance at line 55) line 55
  10. instance OAI.ContingencyTables.ScalarScheduleProgram.(instance at line 56) line 56
  11. lemma OAI.ContingencyTables.ScalarScheduleProgram.Expr.eval_power line 58
  12. lemma OAI.ContingencyTables.ScalarScheduleProgram.Expr.eval_add line 61
  13. lemma OAI.ContingencyTables.ScalarScheduleProgram.Expr.eval_mul line 63
  14. lemma OAI.ContingencyTables.ScalarScheduleProgram.Expr.eval_ofNat line 65
  15. def OAI.ContingencyTables.ScalarScheduleProgram.vector line 68
  16. def OAI.ContingencyTables.ScalarScheduleProgram.vectorRealizer line 70
  17. lemma OAI.ContingencyTables.ScalarScheduleProgram.polynomial_vector line 74