OAI/GroupTheory/PolycyclicRecognition/Geometry/FlowSupportedProfileIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Supported profile increments from one fixed occupation limit

The cutoff is chosen before the occupation limit, which is chosen before the microstep length. Invariance and the stationary estimate remain explicit interfaces to the already proved Cartan occupation and stationary theorems.

  1. theorem OAI.PolycyclicRecognition.supported_profile_increment_of_flow line 22