OAI/Geometry/RCD/Heat/LocalScaledLogSource.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source of any local scaled logarithm

The local L2 source is independent of the chosen extension. In particular a lower bound for that source applies to the original heat representative.

  1. theorem OAI.RegularPointCoordinates.local_scaled_log_source line 21