OAI/Analysis/IrrationalRotation/Spectral/DeterminantWeightBridge.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ScalarDeterminant.regularized_determinant_eq_zero_of_log_integral line 13
2. theorem OAI.Invariant233.IsContinuousCircleWeight.regularized_determinant_eq_zero line 27
3. theorem OAI.Invariant233.fugledeKadisonDeterminant_continuous_circle_weight line 38
4. theorem OAI.Invariant233.fugledeKadisonDeterminant_real_circle_weight line 46
5. theorem OAI.Invariant233.fugledeKadisonDeterminant_unitary_real_circle_weight line 58