OAI/Geometry/RCD/Transport/CompactContactCompletion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact contact completion by two quadratic transforms

The completion preserves every contact of the original compact potential. It also keeps an explicit compact support radius for the right potential.

  1. theorem OAI.RegularPointCoordinates.compact_contact_completion line 18