OAI/Analysis/LipschitzHilbert/Geometry/FarPairEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Total far-pair energy, charged to the earlier rectangle.

  1. theorem OAI.LipschitzHilbert.far_outgoing_sum line 12
  2. theorem OAI.LipschitzHilbert.selected_far_energy line 51