OAI/Analysis/SymmetricDomains/EulerSpectrum.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Release061.Biholomorph.WeightedLieModel line 49
2. abbrev OAI.Release061.Biholomorph.WeightedLieModel.point line 81
3. abbrev OAI.Release061.Biholomorph.WeightedLieModel.u line 82
4. abbrev OAI.Release061.Biholomorph.WeightedLieModel.E line 83
5. abbrev OAI.Release061.Biholomorph.WeightedLieModel.T line 84
6. abbrev OAI.Release061.Biholomorph.WeightedLieModel.H line 85
7. theorem OAI.Release061.Biholomorph.WeightedLieModel.eq_of_germ line 87
8. theorem OAI.Release061.Biholomorph.WeightedLieModel.lie_germ line 96
9. theorem OAI.Release061.Biholomorph.WeightedLieModel.translation_euler line 105
10. theorem OAI.Release061.Biholomorph.WeightedLieModel.translation_rotation line 112
11. def OAI.Release061.Biholomorph.WeightedLieModel.center line 119
12. theorem OAI.Release061.Biholomorph.WeightedLieModel.center_euler line 122
13. theorem OAI.Release061.Biholomorph.WeightedLieModel.center_rotation line 126
14. theorem OAI.Release061.Biholomorph.WeightedLieModel.center_translation line 129
15. theorem OAI.Release061.Biholomorph.WeightedLieModel.centered_euler_germ line 132
16. theorem OAI.Release061.Biholomorph.WeightedLieModel.centered_rotation_germ line 138
17. theorem OAI.Release061.Biholomorph.WeightedLieModel.euler_semisimple line 144
18. theorem OAI.Release061.Biholomorph.WeightedLieModel.euler_extreme_rotation line 149
19. theorem OAI.Release061.Biholomorph.WeightedLieModel.euler_extreme_zero line 157
20. theorem OAI.Release061.Biholomorph.WeightedLieModel.euler_spectrum line 167