OAI/Combinatorics/ContingencyTables/Dense/DenseRational.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact rational evaluation of the dense bin exponent

Only integer completion, rational comparison and division are needed to compute a bin's weight exponent. The real penalty used in the geometric proof is exactly the cast of this finite rational maximum.

  1. def OAI.ContingencyTables.GridBoundary.cornerFree line 20
  2. theorem OAI.ContingencyTables.GridBoundary.cornerFree_cast line 25
  3. theorem OAI.ContingencyTables.GridBoundary.corner_integerTable_cast line 34
  4. def OAI.ContingencyTables.GridBoundary.rationalComponent line 43
  5. def OAI.ContingencyTables.GridBoundary.rationalPenalty line 50
  6. theorem OAI.ContingencyTables.GridBoundary.rationalPenalty_nonnegative line 54
  7. theorem OAI.ContingencyTables.GridBoundary.rationalComponent_cast line 60
  8. theorem OAI.ContingencyTables.GridBoundary.rationalPenalty_cast line 79
  9. def OAI.ContingencyTables.GridBoundary.denseExponent line 89
  10. theorem OAI.ContingencyTables.GridBoundary.denseExponent_eq_floor line 93
  11. theorem OAI.ContingencyTables.GridBoundary.denseBinWeight_eq_dyadic line 104