OAI/Geometry/EinsteinFour/FlowTimeReversal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The first-variation criterion also applies at negative times, by reversing the actual autonomous equation.

  1. theorem OAI.PositiveEinsteinFour.FlowCalculus.hasFDerivAt_flow_endpoint_nonpos line 17