OAI/Geometry/RCD/Transport/RenyiLocalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Localization of finite Rényi integrals

The reference measure is restricted only for compactness arguments. The resulting values agree with the original Hausdorff-reference integrals, including for supported measures which have a singular part.

  1. theorem OAI.RegularPointCoordinates.renyiPower_localized line 18
  2. theorem OAI.RegularPointCoordinates.renyiIntegral_localized line 40