OAI/Geometry/RCD/Heat/CompactTimePairingDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The time derivative in the compact Hamilton--Jacobi pairing

The original pairing need only be Lipschitz on the open interval. A Lipschitz extension defines its endpoint values; the zero boundary time test removes those values from integration by parts.

  1. theorem OAI.RegularPointCoordinates.compact_time_pairing_derivative_identity line 17