OAI/Geometry/RCD/Transport/RenyiDyadicChord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional scalar chord along the fixed dyadic tree

This is Rajala's preliminary estimate (3.1), retaining the dimension in the exact reduced coefficient. It will provide endpoint entropy continuity.

  1. theorem OAI.RegularPointCoordinates.FollowsRenyiTree.reducedChord line 20