OAI/Geometry/RCD/Sobolev/ScaledCompactFactorGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform gradients of the actual small-noise logarithmic potentials

Both the potential and its weak source are scaled before taking limits. The bound is uniform over noise parameters in (0,1] and interior times.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_scaled_gradient line 21