OAI/NumberTheory/Ostmann/Construction/InitialEtaState.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.InitialEta.jointOutside line 17
2. def OAI.Ostmann.Construction.InitialEta.jointState line 20
3. theorem OAI.Ostmann.Construction.InitialEta.jointOutside_length line 24
4. theorem OAI.Ostmann.Construction.InitialEta.jointState_matches line 28
5. theorem OAI.Ostmann.Construction.InitialEta.jointState_plus line 32
6. theorem OAI.Ostmann.Construction.InitialEta.jointState_minus line 35
7. theorem OAI.Ostmann.Construction.InitialEta.jointState_small_value line 38
8. theorem OAI.Ostmann.Construction.InitialEta.jointOutside_value line 50
9. theorem OAI.Ostmann.Construction.InitialEta.initialCoordinates_ext line 60
10. theorem OAI.Ostmann.Construction.InitialEta.jointState_coordinates line 67
11. theorem OAI.Ostmann.Construction.InitialEta.jointState_bins line 92
12. theorem OAI.Ostmann.Construction.InitialEta.jointState_prime line 98