OAI/Analysis/JiangSu/CentralSequences/QuasicentralResolvent.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Quasicentral.resolvent line 16
  2. lemma OAI.Quasicentral.resolvent_nonneg line 17
  3. lemma OAI.Quasicentral.resolvent_norm_lt_one line 18
  4. lemma OAI.Quasicentral.resolvent_le_one line 19
  5. lemma OAI.Quasicentral.resolvent_mono line 21
  6. lemma OAI.Quasicentral.conjugate_mono line 24
  7. lemma OAI.Quasicentral.conjugate_resolvent line 29
  8. lemma OAI.Quasicentral.conjugate_star_cancel line 37
  9. lemma OAI.Quasicentral.conjugate_one line 44
  10. lemma OAI.Quasicentral.selfadjoint_norm_le_of_order_bounds line 47
  11. def OAI.Quasicentral.logarithmicAverage line 62
  12. lemma OAI.Quasicentral.logarithmicAverage_nonneg line 65
  13. lemma OAI.Quasicentral.logarithmicAverage_le_one line 70
  14. lemma OAI.Quasicentral.logarithmicAverage_conjugate_le line 78
  15. lemma OAI.Quasicentral.logarithmicAverage_commutator_bound line 110
  16. lemma OAI.Quasicentral.nnreal_cfc_mem line 141
  17. def OAI.Quasicentral.inverseResolvent line 147
  18. lemma OAI.Quasicentral.inverseResolvent_nonneg line 148
  19. lemma OAI.Quasicentral.resolvent_inverseResolvent line 149
  20. lemma OAI.Quasicentral.logarithmicAverage_dominates line 169
  21. theorem OAI.Quasicentral.exists_logarithmic_contraction line 182