OAI/Geometry/RCD/Heat/CompactHeatReferenceMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual reference normalization for a uniform compact endpoint law

If the reference point lies in an interior ball of the support, its heat factor with constant endpoint weight stays between two fixed positive constants at small times. Hence its scaled logarithm tends to zero.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_reference_mass line 24
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_reference_scaled_log line 61