OAI/Geometry/RCD/Transport/BranchEntropyDeficit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The quantitative entropy deficit of a separated branch

This is the scalar rearrangement in the branching argument of Rajala--Sturm, arXiv:1207.6754, proof of Theorem 1.1, pp. 10--11. The three chord inequalities retain the curvature error and the separation entropy explicitly.

  1. theorem OAI.RegularPointCoordinates.branch_entropy_deficit line 17
  2. theorem OAI.RegularPointCoordinates.branch_entropy_deficit_of_lower_bound line 31
  3. theorem OAI.RegularPointCoordinates.tendsto_branch_entropy_budget line 41
  4. theorem OAI.RegularPointCoordinates.exists_small_branch_budget line 56