OAI/Analysis/IrrationalRotation/Spectral/QuasinilpotentCommuting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.exists_geometric_bound_of_root_tendsto_zero line 14
2. theorem OAI.Invariant233.root_tendsto_zero_of_geometric_bounds line 38
3. theorem OAI.Invariant233.NormQuasinilpotent.geometric_bound line 67
4. theorem OAI.Invariant233.NormQuasinilpotent.mul_of_commute line 72
5. theorem OAI.Invariant233.norm_add_pow_le_of_geometric_bounds line 87
6. theorem OAI.Invariant233.NormQuasinilpotent.add_of_commute line 115