OAI/Analysis/IrrationalRotation/Spectral/CFCLogSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.CFCLogSeries.term line 13
2. lemma OAI.Invariant233.CFCLogSeries.norm_term_le line 16
3. lemma OAI.Invariant233.CFCLogSeries.summable_term line 23
4. lemma OAI.Invariant233.CFCLogSeries.spectrum_abs_lt_one line 33
5. theorem OAI.Invariant233.CFCLogSeries.hasSum_neg_log_one_sub line 37
6. theorem OAI.Invariant233.CFCLogSeries.norm_log_remainder_le line 79
7. theorem OAI.Invariant233.CFCLogSeries.norm_log_one_sub_add_le line 97
8. theorem OAI.Invariant233.CFCLogSeries.norm_log_one_add_sub_le line 101
9. theorem OAI.Invariant233.CFCLogSeries.TracialState_hasSum_log line 106
10. theorem OAI.Invariant233.CFCLogSeries.norm_trace_log_one_add_sub_le line 112