OAI/Geometry/RCD/Transport/RenyiNodeChildren.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The two children of a fixed maximal transport midpoint

  1. def OAI.RegularPointCoordinates.RenyiNodeSplit.children line 15
  2. def OAI.RegularPointCoordinates.RenyiNodeSplit.leftNode line 69
  3. def OAI.RegularPointCoordinates.RenyiNodeSplit.rightNode line 72
  4. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.leftNode_left line 75
  5. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.leftNode_right line 77
  6. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.rightNode_left line 79
  7. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.rightNode_right line 81
  8. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.leftNode_capacity line 83
  9. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.rightNode_capacity line 85
  10. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.leftNode_distance line 87
  11. theorem OAI.RegularPointCoordinates.RenyiNodeSplit.rightNode_distance line 89