OAI/Combinatorics/ContingencyTables/Dense/DenseLocalGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Feasible bins and exponent bounds for dense rejection

These bounds use the actual quotient widths and margin-derived penalty. In particular, every bin containing a feasible point has weight one.

  1. theorem OAI.ContingencyTables.DenseAffine.densePenalty_change line 21
  2. theorem OAI.ContingencyTables.DenseAffine.densePenalty_cube_bound line 40
  3. theorem OAI.ContingencyTables.DenseAffine.densePenalty_corner_zero line 60
  4. theorem OAI.ContingencyTables.GridBoundary.denseGridSize_pos line 97
  5. theorem OAI.ContingencyTables.GridBoundary.denseBinWeight_eq_one line 101
  6. theorem OAI.ContingencyTables.GridBoundary.denseBinWeight_le_one line 116
  7. theorem OAI.ContingencyTables.GridBoundary.denseBinWeight_lower line 131
  8. theorem OAI.ContingencyTables.GridBoundary.grid_card line 158
  9. theorem OAI.ContingencyTables.GridBoundary.denseBinChain_pi_lower line 165