OAI/Geometry/RCD/Transport/RenyiIntegralAdditivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact extended Rényi additivity for finite length decompositions

This version works against the full sigma-finite reference measure. No localization or finiteness of the reference volume is required.

  1. theorem OAI.RegularPointCoordinates.renyiIntegral_add_mutuallySingular line 17
  2. theorem OAI.RegularPointCoordinates.renyiIntegral_finset_additive line 32
  3. theorem OAI.RegularPointCoordinates.renyiIntegral_smul line 57