OAI/Geometry/RCD/Sobolev/ScaledCompactFactorLipschitz.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform local Lipschitz bounds for small-noise heat potentials

The local weak-gradient estimate applies to the prescribed continuous logarithm, so no noise-dependent choice of representative is made.

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