OAI/Geometry/RCD/Metric/CompactFactorScaledSource.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform lower weak sources for scaled compact-factor logarithms

The source and gradient belong to the same local logarithm. The constants are independent of the endpoint factor and of its normalization.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_scaled_source line 24