OAI/Combinatorics/ContingencyTables/Machines/BinPopulationProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Computing the exact population correction in binary

The program multiplies one interval size and one full-range denominator per free coordinate. It never lists the integer assignments in a bin.

  1. def OAI.ContingencyTables.BinPopulationProgram.factorNumerator line 18
  2. def OAI.ContingencyTables.BinPopulationProgram.factorNumeratorRealizer line 20
  3. lemma OAI.ContingencyTables.BinPopulationProgram.polynomial_factorNumerator line 24
  4. def OAI.ContingencyTables.BinPopulationProgram.numerator line 29
  5. def OAI.ContingencyTables.BinPopulationProgram.numeratorRealizer line 30
  6. lemma OAI.ContingencyTables.BinPopulationProgram.polynomial_numerator line 31
  7. def OAI.ContingencyTables.BinPopulationProgram.denominator line 34
  8. def OAI.ContingencyTables.BinPopulationProgram.denominatorRealizer line 35
  9. lemma OAI.ContingencyTables.BinPopulationProgram.polynomial_denominator line 37
  10. def OAI.ContingencyTables.BinPopulationProgram.output line 41
  11. def OAI.ContingencyTables.BinPopulationProgram.outputRealizer line 43
  12. theorem OAI.ContingencyTables.BinPopulationProgram.polynomial_output line 45
  13. lemma OAI.ContingencyTables.BinPopulationProgram.output_ofFn line 49
  14. def OAI.ContingencyTables.BinPopulationProgram.data line 64
  15. theorem OAI.ContingencyTables.BinPopulationProgram.output_data line 70
  16. theorem OAI.ContingencyTables.BinPopulationProgram.output_integerBin line 99