OAI/Geometry/RCD/Heat/CompactScalingBoundary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact logarithmic boundary identities for compact heat scaling

These identities use the actual normalization equations of the positive kernel scaling pair. The reference-time gauge cancels in differences.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_scaling_log_boundary line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_scaling_centered_boundary line 31