OAI/Analysis/Commutator/FiniteHankel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FreeCorner.compress line 22
  2. lemma OAI.Kadison.FreeCorner.norm_compress_le line 25
  3. lemma OAI.Kadison.FreeCorner.compression_commutator_identity line 38
  4. lemma OAI.Kadison.FreeCorner.norm_compression_commutator_le line 51
  5. lemma OAI.Kadison.FreeCorner.compressed_commutator_bound line 95
  6. lemma OAI.Kadison.FiniteCompression.inner_sum_diagonal line 123
  7. lemma OAI.Kadison.FiniteCompression.norm_sum_sq line 132
  8. def OAI.Kadison.FiniteCompression.average line 137
  9. lemma OAI.Kadison.FiniteCompression.average_apply line 141
  10. lemma OAI.Kadison.FiniteCompression.average_inner line 145
  11. def OAI.Kadison.FiniteCompression.averageIsometry line 160
  12. lemma OAI.Kadison.FiniteCompression.averageIsometry_toCLM line 170
  13. lemma OAI.Kadison.FiniteCompression.norm_average_le line 175
  14. lemma OAI.Kadison.FiniteCompression.comp_sum' line 196
  15. lemma OAI.Kadison.FiniteCompression.sum_comp' line 202
  16. lemma OAI.Kadison.FiniteCompression.average_error line 208
  17. lemma OAI.Kadison.FiniteCompression.average_compression line 215
  18. lemma OAI.Kadison.FiniteCompression.average_compression_entries line 229
  19. theorem OAI.Kadison.FiniteHankel.norm_commutator_le_of_finite_entries line 255