OAI/Geometry/RCD/Heat/CompactHeatJointLogLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact logarithmic cost of the joint heat bridge

The limit retains both legs of the broken path. It is uniform on each compact set of intermediate points, with the original endpoint potentials.

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointSlack line 25
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.jointSlack_continuous line 30
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.joint_log_limit line 37