OAI/Geometry/PolarProducts/PolarApproximation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SymmetricPolar.exists_positive_slack line 44
  2. theorem OAI.SymmetricPolar.finite_strips_embedding line 51
  3. theorem OAI.ConvexPolar.zero_mem_interior_of_symmetric line 123
  4. theorem OAI.ConvexPolar.isClosed_polar line 136
  5. theorem OAI.ConvexPolar.polar_abs_pairing line 141
  6. theorem OAI.ConvexPolar.norm_smul_normalized line 148
  7. theorem OAI.ConvexPolar.normalized_inner line 152
  8. theorem OAI.ConvexPolar.norm_le_of_mem_polar line 157
  9. theorem OAI.ConvexPolar.isCompact_polar line 167
  10. theorem OAI.ConvexPolar.mem_polar_polar_iff line 178
  11. theorem OAI.ConvexPolar.closedBall_subset_polar_of_norm_bound line 200
  12. theorem OAI.ConvexPolar.pairing_le_of_net line 220
  13. theorem OAI.ConvexPolar.net_norm_bound line 230
  14. theorem OAI.ConvexPolar.finite_polar_approximation line 241
  15. theorem OAI.SymmetricPolar.symmetric_polar_embedding line 305