OAI/Geometry/RCD/Heat/CompactHeatOsmoticGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform local gradient bound for any osmotic representative

Locality makes this bound apply to the actual representatives used in second variation, independent of the chosen compact extension.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.osmotic_local_gradient line 25