OAI/Geometry/RCD/Heat/CompactFactorLogGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quadratic growth of the logarithmic heat-factor gradient

The constants are independent of the endpoint scaling function and its amplitude. This is the short-time specialization of the estimate used in Gigli--Tamanini, JEMS 23 (2021), Theorem 3.3. The local logarithm and its weak Laplacian are constructed on each compact region.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_log_gradient line 24