OAI/Probability/LatticeSurface/Convexity/FreeHilbert.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ConvexSkorokhod.project_norm_min line 11
  2. abbrev OAI.ProjectionComparison.FreeSpace line 31
  3. def OAI.ProjectionComparison.freeCoordinates line 33
  4. def OAI.ProjectionComparison.extendFree line 35
  5. def OAI.ProjectionComparison.freeCarrier line 38
  6. lemma OAI.ProjectionComparison.extendFree_coordinates line 52
  7. lemma OAI.ProjectionComparison.extendFree_continuous line 60
  8. lemma OAI.ProjectionComparison.extendFree_combo line 68
  9. lemma OAI.ProjectionComparison.freeCarrier_closed line 77
  10. lemma OAI.ProjectionComparison.freeCarrier_convex line 81
  11. lemma OAI.ProjectionComparison.objective_free line 94
  12. theorem OAI.ProjectionComparison.exists_free_body line 117