OAI/Geometry/RCD/Transport/RenyiFiniteAdditivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite length decomposition of the Rényi integral

  1. theorem OAI.RegularPointCoordinates.mutuallySingular_finset_sum_right line 14
  2. theorem OAI.RegularPointCoordinates.renyiPower_finset_additive line 24