OAI/Geometry/RCD/Heat/CanonicalMovingLogLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp small-noise lower action along converging endpoint sequences

A hypothetical bad sequence is compared with a uniform law on a small ball. Its constructed heat limit supplies the sharp main action; the rough Gaussian bound is used only on the short final step. Both errors are made arbitrarily small before taking the subsequence.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_moving_log_lower line 27