OAI/Combinatorics/ContingencyTables/Machines/FractionAggregateProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial exact fraction averages and products

These are the arithmetic folds used by the executed weight estimator. Normalization makes the average valid on every input, including a raw fraction with denominator zero.

  1. def OAI.ContingencyTables.FractionAggregateProgram.average line 18
  2. def OAI.ContingencyTables.FractionAggregateProgram.averageRealizer line 20
  3. lemma OAI.ContingencyTables.FractionAggregateProgram.polynomial_average line 25
  4. lemma OAI.ContingencyTables.FractionAggregateProgram.average_value line 31
  5. lemma OAI.ContingencyTables.FractionAggregateProgram.average_ofFn line 41
  6. lemma OAI.ContingencyTables.FractionAggregateProgram.height_mul line 48
  7. lemma OAI.ContingencyTables.FractionAggregateProgram.fold_height line 65
  8. lemma OAI.ContingencyTables.FractionAggregateProgram.polynomial_productFold line 78
  9. def OAI.ContingencyTables.FractionAggregateProgram.product line 97
  10. def OAI.ContingencyTables.FractionAggregateProgram.productRealizer line 99
  11. lemma OAI.ContingencyTables.FractionAggregateProgram.polynomial_product line 104
  12. lemma OAI.ContingencyTables.FractionAggregateProgram.fold_value line 108
  13. lemma OAI.ContingencyTables.FractionAggregateProgram.product_value line 117