OAI/Analysis/Commutator/OperatorAmplification.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.OperatorAmplification.SumSpace line 21
  2. def OAI.Kadison.OperatorAmplification.single line 23
  3. lemma OAI.Kadison.OperatorAmplification.single_apply line 28
  4. def OAI.Kadison.OperatorAmplification.diagonal line 32
  5. lemma OAI.Kadison.OperatorAmplification.diagonal_apply line 48
  6. lemma OAI.Kadison.OperatorAmplification.diagonal_single line 51
  7. lemma OAI.Kadison.OperatorAmplification.sum_single line 57
  8. def OAI.Kadison.OperatorAmplification.entry line 61
  9. lemma OAI.Kadison.OperatorAmplification.entry_apply line 65
  10. lemma OAI.Kadison.OperatorAmplification.apply_eq_sum_entries line 69
  11. lemma OAI.Kadison.OperatorAmplification.reconstruct line 75
  12. lemma OAI.Kadison.OperatorAmplification.entry_commutes line 80
  13. lemma OAI.Kadison.OperatorAmplification.commutes_of_entries line 87
  14. lemma OAI.Kadison.OperatorAmplification.diagonal_bicommutant line 98
  15. theorem OAI.Kadison.OperatorAmplification.bicommutant_finite_approx line 108