OAI/Geometry/RCD/Sobolev/CompactFactorScaledEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative energy of the original compact heat factors

The coefficient is independent of the scaling function, noise and compact region. No derivative of a logarithmic extension remains in the conclusion.

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