OAI/Geometry/RCD/Heat/CompactHeatHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Hessian second variation for the original compact heat factors

A single pair of initial L2 functions represents the original endpoint factors for every positive time. Their pairing has the computed second derivative on the whole open interpolation interval.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_bridge_hessian line 22