OAI/Analysis/IrrationalRotation/Spectral/Spectral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.spectralRadius_eq_zero_of_normRoot_tendsto line 16
2. theorem OAI.Invariant233.spectrum_eq_singleton_zero_of_normRoot_tendsto line 24
3. theorem OAI.Invariant233.exp_half_log_eq_sqrt line 44
4. theorem OAI.Invariant233.iInf_sqrt_sq_add_pos line 48
5. theorem OAI.Invariant233.logarithmicPotentialDeterminant_dirac line 73
6. theorem OAI.Invariant233.TracialState.map_real line 87
7. theorem OAI.Invariant233.fugledeKadisonDeterminant_zero line 92
8. theorem OAI.Invariant233.fugledeKadisonDeterminant_unitary_mul line 103