OAI/Geometry/RCD/Coordinates/ScalingNormalizationLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar normalization of a positive compact kernel scaling pair

The exact row identity and the proved compact Laplace limit determine the otherwise free sum of the two logarithmic gauges.

  1. theorem OAI.RegularPointCoordinates.scaling_normalization_limit line 20