OAI/Combinatorics/ContingencyTables/Dense/DenseGoodBins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Wholly feasible bins covering the inner polytope

  1. def OAI.ContingencyTables.GridBoundary.closedBinSet line 17
  2. theorem OAI.ContingencyTables.GridBoundary.mem_closedBinSet line 20
  3. theorem OAI.ContingencyTables.GridBoundary.closedBinSet_volume line 28
  4. def OAI.ContingencyTables.GridBoundary.goodBin line 32
  5. def OAI.ContingencyTables.GridBoundary.goodBins line 36
  6. def OAI.ContingencyTables.GridBoundary.denseGridInner line 40
  7. theorem OAI.ContingencyTables.GridBoundary.inner_bin_good line 44
  8. theorem OAI.ContingencyTables.GridBoundary.goodBin_weight_one line 68
  9. theorem OAI.ContingencyTables.GridBoundary.dense_inner_covered_by_good_bins line 76
  10. theorem OAI.ContingencyTables.GridBoundary.goodBins_volume_lower line 107