OAI/Geometry/RCD/Heat/CompactHeatStrongGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strong local gradients of the actual fixed-gauge heat potentials

Uniform convergence of values now implies convergence of local gradient differences. The local L1 source bound is constructed from the RCD heat estimates, rather than supplied as a compactness premise.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_strong_gradient line 23