OAI/Geometry/RCD/Transport/LengthComponentIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact Rényi sums for finite length partitions

Disjoint length bins give disjoint spatial components at every interior time. No such assertion is made at the two endpoints.

  1. theorem OAI.RegularPointCoordinates.sum_length_restrictions line 18
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.length_partition_renyiIntegral line 37