OAI/Combinatorics/ContingencyTables/Dense/DenseRegionVolume.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Inner-polytope and penalty-sublevel volume for the actual margins

  1. def OAI.ContingencyTables.DenseAffine.normalizedOffset line 17
  2. def OAI.ContingencyTables.DenseAffine.normalizedCoeff line 21
  3. def OAI.ContingencyTables.DenseAffine.normalizedRegion line 26
  4. theorem OAI.ContingencyTables.DenseAffine.normalizedRegion_eq_affine line 29
  5. theorem OAI.ContingencyTables.DenseAffine.normalizedEntry_continuous line 38
  6. theorem OAI.ContingencyTables.DenseAffine.normalizedRegion_closed line 48
  7. theorem OAI.ContingencyTables.DenseAffine.normalizedRegion_zero line 58
  8. theorem OAI.ContingencyTables.DenseAffine.dense_feasible_compact line 76
  9. theorem OAI.ContingencyTables.DenseAffine.dense_inner_contraction line 88
  10. theorem OAI.ContingencyTables.DenseAffine.dense_inner_volume line 119
  11. theorem OAI.ContingencyTables.DenseAffine.dense_relaxed_volume line 144
  12. theorem OAI.ContingencyTables.DenseAffine.dense_sublevel_volume line 163