OAI/RingTheory/BassTrace/AffinePotentials.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Finite affine branch geometry for the exact transport metric and compatible cuts.

  1. def OAI.BassTrace.Sparse.halfspacePolyhedron line 15
  2. def OAI.BassTrace.Sparse.activeConstraints line 18
  3. lemma OAI.BassTrace.Sparse.mem_activeConstraints line 21
  4. lemma OAI.BassTrace.Sparse.exists_extrapolate_mem line 26
  5. lemma OAI.BassTrace.Sparse.activeConstraints_injOn_extremePoints line 53
  6. lemma OAI.BassTrace.Sparse.finite_extremePoints_halfspacePolyhedron line 69
  7. def OAI.BassTrace.Sparse.polyhedronVertices line 76
  8. lemma OAI.BassTrace.Sparse.mem_polyhedronVertices line 79
  9. lemma OAI.BassTrace.Sparse.exists_extreme_maximizer line 89
  10. lemma OAI.BassTrace.Sparse.exists_vertex_maximizer line 97
  11. lemma OAI.BassTrace.Sparse.halfspacePolyhedron_eq_convexHull_vertices line 103
  12. def OAI.BassTrace.Sparse.potentialSet line 129
  13. def OAI.BassTrace.Sparse.potentialLinear line 132
  14. def OAI.BassTrace.Sparse.potentialBound line 137
  15. lemma OAI.BassTrace.Sparse.potentialSet_eq_halfspacePolyhedron line 141
  16. lemma OAI.BassTrace.Sparse.zero_mem_potentialSet line 158
  17. lemma OAI.BassTrace.Sparse.isClosed_potentialSet line 161
  18. def OAI.BassTrace.Sparse.totalDistances line 172
  19. lemma OAI.BassTrace.Sparse.totalDistances_nonneg line 174
  20. lemma OAI.BassTrace.Sparse.dist_le_totalDistances line 177
  21. lemma OAI.BassTrace.Sparse.potential_coordinate_bound line 183
  22. lemma OAI.BassTrace.Sparse.isCompact_potentialSet line 203
  23. def OAI.BassTrace.Sparse.potentialVertices line 211
  24. lemma OAI.BassTrace.Sparse.mem_potentialVertices line 214
  25. lemma OAI.BassTrace.Sparse.potentialVertices_subset line 218
  26. lemma OAI.BassTrace.Sparse.exists_potential_vertex_maximizer line 221
  27. def OAI.BassTrace.Sparse.centerPotential line 226
  28. lemma OAI.BassTrace.Sparse.centerPotential_mem line 229
  29. def OAI.BassTrace.Sparse.potentialPairing line 246
  30. lemma OAI.BassTrace.Sparse.potentialPairing_apply line 250
  31. lemma OAI.BassTrace.Sparse.pairing_centerPotential line 256
  32. lemma OAI.BassTrace.Sparse.lipschitz_potential line 262
  33. lemma OAI.BassTrace.Sparse.exists_global_potential_extension line 271
  34. lemma OAI.BassTrace.Sparse.exists_global_vertex_maximizer line 287
  35. def OAI.BassTrace.Sparse.globalPairingValues line 307
  36. lemma OAI.BassTrace.Sparse.global_dual_eq_finite_vertex_max line 310