OAI/Dynamics/EntropyCounterexample/RealizedRegisterRegularity.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem340.Construction.analyticClockHomeomorph_eq_modelline 10 - theorem
OAI.Problem340.Construction.registerInputInStandardCoordinates_modelHomeomorphline 13 - theorem
OAI.Problem340.Construction.realizedMap_register_eq_standardOutputline 21 - theorem
OAI.Problem340.Construction.realizedMap_register_hasLocalC1Extensionline 27