OAI/Combinatorics/ContingencyTables/Machines/CorrectionValueProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Binary composition of the correction value

The input contains the computed grid exponent, phase ratio, point penalty, population factor and two precision marker lists. Normalized fraction multiplication supplies a positive denominator for the signed exponent passed to the executed power approximation.

  1. abbrev OAI.ContingencyTables.CorrectionValueProgram.Frame line 17
  2. def OAI.ContingencyTables.CorrectionValueProgram.weighted line 19
  3. def OAI.ContingencyTables.CorrectionValueProgram.weightedRealizer line 20
  4. lemma OAI.ContingencyTables.CorrectionValueProgram.polynomial_weighted line 23
  5. def OAI.ContingencyTables.CorrectionValueProgram.exponentInput line 27
  6. def OAI.ContingencyTables.CorrectionValueProgram.exponentInputRealizer line 29
  7. lemma OAI.ContingencyTables.CorrectionValueProgram.polynomial_exponentInput line 35
  8. lemma OAI.ContingencyTables.CorrectionValueProgram.weighted_denominator_pos line 43
  9. lemma OAI.ContingencyTables.CorrectionValueProgram.exponentInput_value line 46
  10. abbrev OAI.ContingencyTables.CorrectionValueProgram.Input line 56
  11. def OAI.ContingencyTables.CorrectionValueProgram.powerInput line 58
  12. def OAI.ContingencyTables.CorrectionValueProgram.powerInputRealizer line 60
  13. lemma OAI.ContingencyTables.CorrectionValueProgram.polynomial_powerInput line 62
  14. def OAI.ContingencyTables.CorrectionValueProgram.power line 67
  15. def OAI.ContingencyTables.CorrectionValueProgram.powerRealizer line 68
  16. lemma OAI.ContingencyTables.CorrectionValueProgram.polynomial_power line 71
  17. def OAI.ContingencyTables.CorrectionValueProgram.output line 74
  18. def OAI.ContingencyTables.CorrectionValueProgram.outputRealizer line 75
  19. theorem OAI.ContingencyTables.CorrectionValueProgram.polynomial_output line 78
  20. theorem OAI.ContingencyTables.CorrectionValueProgram.output_value line 82
  21. theorem OAI.ContingencyTables.CorrectionValueProgram.output_approximate line 96