OAI/Analysis/MetricEntropy/ConvexBody.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The concrete symmetric convex bodies

The absolute row hull is the convex hull of the actual finite set of rows and their negatives. Adding a positive multiple of the coordinate cube gives full ambient interior, without any spanning hypothesis on the rows.

  1. theorem OAI.MetricEntropyDuality.cube_eq_closedBall line 27
  2. theorem OAI.MetricEntropyDuality.isCompact_cube line 34
  3. theorem OAI.MetricEntropyDuality.convex_cube line 38
  4. theorem OAI.MetricEntropyDuality.cube_symmetric line 43
  5. theorem OAI.MetricEntropyDuality.zero_mem_interior_cube line 46
  6. theorem OAI.MetricEntropyDuality.cube_isSymmetricConvexBody line 50
  7. theorem OAI.MetricEntropyDuality.zero_mem_interior_smul_cube line 56
  8. theorem OAI.MetricEntropyDuality.convex_absRowHull line 68
  9. theorem OAI.MetricEntropyDuality.absRowHull_symmetric line 71
  10. theorem OAI.MetricEntropyDuality.zero_mem_absRowHull line 89
  11. theorem OAI.MetricEntropyDuality.isCompact_absRowHull line 98
  12. theorem OAI.MetricEntropyDuality.convex_matrixBody line 108
  13. theorem OAI.MetricEntropyDuality.isCompact_matrixBody line 111
  14. theorem OAI.MetricEntropyDuality.matrixBody_symmetric line 115
  15. theorem OAI.MetricEntropyDuality.smul_cube_subset_matrixBody line 130
  16. theorem OAI.MetricEntropyDuality.matrixBody_three_row_mem line 138
  17. theorem OAI.MetricEntropyDuality.zero_mem_interior_matrixBody line 145
  18. theorem OAI.MetricEntropyDuality.matrixBody_isSymmetricConvexBody line 150