OAI/Geometry/RCD/Transport/RenyiTransportNode.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed nodes for compatible Rényi refinement

A node records only the bounded transport data needed at that segment. Its selected maximal midpoint is independent of any requested tree depth.

  1. structure OAI.RegularPointCoordinates.RenyiTransportNode line 18
  2. structure OAI.RegularPointCoordinates.RenyiNodeSplit line 36
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.renyiNodeSplit_nonempty line 45
  4. def OAI.RegularPointCoordinates.NoncollapsedRCD.selectedRenyiSplit line 56