OAI/Analysis/JiangSu/CentralSequences/NormUltrapowerToTracial.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NonunitalGamma.normNull_uniformNull line 20
  2. def OAI.NonunitalGamma.normToTracial line 28
  3. lemma OAI.NonunitalGamma.normToTracial_mk line 52
  4. lemma OAI.NonunitalGamma.normToTracial_surjective line 55
  5. def OAI.NonunitalGamma.boundedConstant line 61
  6. lemma OAI.NonunitalGamma.boundedConstant_apply line 70
  7. def OAI.NonunitalGamma.normInclusion line 72
  8. lemma OAI.NonunitalGamma.normToTracial_inclusion line 74
  9. def OAI.Quasicentral.conjugate line 86
  10. lemma OAI.Quasicentral.conjugate_apply line 90
  11. lemma OAI.Quasicentral.conjugate_nonneg line 92
  12. lemma OAI.Quasicentral.norm_conjugate line 95
  13. def OAI.Quasicentral.expansionConstant line 99
  14. lemma OAI.Quasicentral.expansionConstant_pos line 101
  15. lemma OAI.Quasicentral.expansionConstant_ne_zero line 103
  16. def OAI.Quasicentral.averageMap line 104
  17. lemma OAI.Quasicentral.averageMap_apply line 106
  18. lemma OAI.Quasicentral.averageMap_nonneg line 108
  19. lemma OAI.Quasicentral.averageMap_norm_le line 113
  20. lemma OAI.Quasicentral.iterate_nonneg line 125
  21. lemma OAI.Quasicentral.iterate_norm_le line 133
  22. lemma OAI.Quasicentral.iterate_summable line 144
  23. theorem OAI.Quasicentral.exists_invariant_domination line 148