OAI/Analysis/LipschitzHilbert/Geometry/RectanglePairEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Ordered overlap sums for an actual finite selection list.

  1. def OAI.LipschitzHilbert.orderedPairSum line 12
  2. def OAI.LipschitzHilbert.previousPairSum line 16
  3. def OAI.LipschitzHilbert.overlapPair line 19
  4. def OAI.LipschitzHilbert.nearPair line 22
  5. def OAI.LipschitzHilbert.farPair line 25
  6. theorem OAI.LipschitzHilbert.overlapPair_split line 29
  7. theorem OAI.LipschitzHilbert.orderedPairSum_split line 35
  8. theorem OAI.LipschitzHilbert.previousPairSum_cons line 41
  9. theorem OAI.LipschitzHilbert.list_overlap_energy line 50