OAI/Geometry/RCD/Heat/CompactHeatJointConcentration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joint bridge limits carry no negative logarithmic slack

The reference measure may have infinite total mass. The argument only uses finite mass on compact intermediate balls, then countable exhaustion.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.joint_negative_mass line 25
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.joint_limit_nonnegative_slack line 59