OAI/Geometry/RCD/Heat/CompactHeatFirstDerivativeLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

First-derivative convergence on the original heat-law subsequence

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.first_derivative_limit line 22