OAI/Geometry/RCD/Heat/ScaledNoiseGradient.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 first term keeps its vanishing noise factor for passage to the action limit.

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