OAI/Combinatorics/ContingencyTables/Counting/CountingBaseProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Executing the capacity-bit and dimension inputs to the counting schedule

  1. abbrev OAI.ContingencyTables.CountingBaseProgram.Input line 12
  2. def OAI.ContingencyTables.CountingBaseProgram.cellBits line 14
  3. def OAI.ContingencyTables.CountingBaseProgram.cellBitsRealizer line 15
  4. lemma OAI.ContingencyTables.CountingBaseProgram.polynomial_cellBits line 18
  5. def OAI.ContingencyTables.CountingBaseProgram.capacityBits line 22
  6. def OAI.ContingencyTables.CountingBaseProgram.capacityBitsRealizer line 24
  7. lemma OAI.ContingencyTables.CountingBaseProgram.polynomial_capacityBits line 29
  8. def OAI.ContingencyTables.CountingBaseProgram.dimension line 35
  9. def OAI.ContingencyTables.CountingBaseProgram.dimensionRealizer line 36
  10. lemma OAI.ContingencyTables.CountingBaseProgram.polynomial_dimension line 41
  11. def OAI.ContingencyTables.CountingBaseProgram.half line 48
  12. def OAI.ContingencyTables.CountingBaseProgram.halfRealizer line 49
  13. lemma OAI.ContingencyTables.CountingBaseProgram.polynomial_half line 52
  14. lemma OAI.ContingencyTables.CountingBaseProgram.half_val line 56
  15. def OAI.ContingencyTables.CountingBaseProgram.frame line 60
  16. def OAI.ContingencyTables.CountingBaseProgram.frameRealizer line 62
  17. lemma OAI.ContingencyTables.CountingBaseProgram.polynomial_frame line 67
  18. def OAI.ContingencyTables.CountingBaseProgram.coefficient line 73
  19. def OAI.ContingencyTables.CountingBaseProgram.coefficientRealizer line 74
  20. lemma OAI.ContingencyTables.CountingBaseProgram.polynomial_coefficient line 77
  21. lemma OAI.ContingencyTables.CountingBaseProgram.capacityBits_data line 80
  22. lemma OAI.ContingencyTables.CountingBaseProgram.dimension_data line 88
  23. lemma OAI.ContingencyTables.CountingBaseProgram.coefficient_data line 92