OAI/Geometry/RCD/Heat/HeatNonlinearPairingDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonlinear forward/backward heat pairing

The two generator terms cancel by the actual weak Laplacian chain rule. Only the second scalar derivative times the gradient square remains.

  1. theorem OAI.RegularPointCoordinates.heat_nonlinear_pairing_hasDerivAt line 19