OAI/Geometry/RCD/Heat/SmallNoiseLogBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing scaled logarithms of uniformly positive bounded masses

  1. theorem OAI.RegularPointCoordinates.small_noise_log_tendsto_zero line 12