OAI/Geometry/RCD/Transport/RenyiDisjointAdditivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Additivity of the Rényi integral on disjoint transport components

Length-localized interior marginals are mutually singular. Their Rényi integrals can therefore be added without losing the finite dimension.

  1. theorem OAI.RegularPointCoordinates.rnDeriv_disjoint_ae line 17
  2. theorem OAI.RegularPointCoordinates.renyiPower_add_mutuallySingular line 39