OAI/Geometry/RCD/Transport/RenyiSubmeasureBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inverse-density lower bounds for a submeasure's Rényi integral

The ambient density can be used even when endpoint length components overlap. Its negative power is smaller than the component density's power.

  1. theorem OAI.RegularPointCoordinates.inverse_density_lintegral_le_renyi line 17