OAI/Geometry/RCD/Transport/ReducedInterpolation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compressed optimal plan with exact reduced interpolation

Finite length components inherit the whole maximal tree. Their scalar interpolation bounds extend by upper semicontinuity, and shrinking the length bins recovers the original endpoint-weighted distortion integral.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_reduced_interpolation line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_reduced_interpolation line 82