OAI/Analysis/IrrationalRotation/Spectral/QuasinilpotentSeries.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.NormQuasinilpotent.eventually_norm_pow_le line 18
  2. theorem OAI.Invariant233.NormQuasinilpotent.summable_norm_smul_pow line 30
  3. theorem OAI.Invariant233.NormQuasinilpotent.summable_smul_pow line 51
  4. theorem OAI.Invariant233.NormQuasinilpotent.summable_norm_logSeries line 58
  5. theorem OAI.Invariant233.NormQuasinilpotent.geometric_inverse_identities line 71
  6. theorem OAI.Invariant233.NormQuasinilpotent.inverse_one_sub_smul line 81
  7. def OAI.Invariant233.vectorTraceContinuousLinearMap line 90
  8. theorem OAI.Invariant233.vectorTraceContinuousLinearMap_apply line 93
  9. theorem OAI.Invariant233.vectorTrace_tsum line 96
  10. theorem OAI.Invariant233.vectorTrace_geometric_series line 103
  11. theorem OAI.Invariant233.vectorTrace_inverse_one_sub_smul line 115
  12. theorem OAI.Invariant233.vectorTrace_resolvent_of_moments_zero line 122
  13. theorem OAI.Invariant233.vectorTrace_logSeries_eq_zero line 144