OAI/Geometry/RCD/Transport/RenyiInverseDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The inverse-density expression for the Rényi integral

  1. theorem OAI.RegularPointCoordinates.renyiIntegral_eq_inverse_density line 13

    Distinct definitions of this name: OAI/Analysis/RCDHeat/RestrictedDensity.lean:66 (different declaration text). Qualify references as OAI.RegularPointCoordinates.renyiIntegral_eq_inverse_density@path.