OAI/Geometry/RCD/Transport/RelativePowerRemainder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A power remainder estimate relative to a possibly small positive density

  1. theorem OAI.RegularPointCoordinates.power_unit_remainder line 12
  2. theorem OAI.RegularPointCoordinates.relative_power_remainder line 23