OAI/Geometry/ProjectionVolume/OuterApproximation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper092.exists_unit_separating_support line 11
  2. theorem OAI.Paper092.unit_support_pos_of_zero_mem_interior line 33
  3. theorem OAI.Paper092.unit_support_le_of_norm_le line 48
  4. theorem OAI.Paper092.norm_le_of_basis_inner_le line 56
  5. theorem OAI.Paper092.subset_interior_smul_of_one_lt line 67
  6. theorem OAI.Paper092.exists_outer_hpolytope_sandwich line 78