OAI/Geometry/RCD/Transport/RenyiDyadicData.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Maximal Rényi midpoints on a finite dyadic tree

These predicates record the actual variational choices of the construction. The reference is always the original measure, independent of support balls.

  1. def OAI.RegularPointCoordinates.RenyiMidpointMaximal line 18
  2. def OAI.RegularPointCoordinates.RenyiDyadicMaximal line 24
  3. theorem OAI.RegularPointCoordinates.RenyiDyadicMaximal.congr line 30