OAI/Analysis/IrrationalRotation/Spectral/ScalarDeterminantZero.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ScalarDeterminant.log_sq_add_sq_le line 15
2. theorem OAI.Invariant233.ScalarDeterminant.integrable_regularized_log line 28
3. theorem OAI.Invariant233.ScalarDeterminant.integrable_truncated_log line 49
4. theorem OAI.Invariant233.ScalarDeterminant.integral_regularized_log_le line 68
5. theorem OAI.Invariant233.ScalarDeterminant.regularized_determinant_eq_zero line 82