OAI/Geometry/RCD/Heat/CompactHeatHessianL1Limit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual logarithmic heat directions have a local Hessian L1 limit

The original convergent heat-action subsequence supplies the directions. Their weak Laplacians, uniform local gradients and strong gradient limit are constructed from the heat equation. No Hessian compactness is assumed.

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