OAI/Analysis/IrrationalRotation/Spectral/DeterminantSemicontinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.continuous_regularizedLog line 17
2. theorem OAI.Invariant233.upperSemicontinuous_fugledeKadisonDeterminant line 28
3. theorem OAI.Invariant233.isOpen_fugledeKadisonDeterminant_lt line 37
4. theorem OAI.Invariant233.continuousAt_fugledeKadisonDeterminant_of_eq_zero line 41
5. theorem OAI.Invariant233.upperSemicontinuous_vectorFugledeKadisonDeterminant line 56
6. theorem OAI.Invariant233.isOpen_vectorFugledeKadisonDeterminant_lt line 65
7. theorem OAI.Invariant233.continuousAt_vectorFugledeKadisonDeterminant_of_eq_zero line 69