OAI/Analysis/Commutator/TensorMultiplicity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.HilbertTensor.pair line 25
  2. lemma OAI.Kadison.HilbertTensor.inner_pair line 27
  3. lemma OAI.Kadison.HilbertTensor.norm_pair line 31
  4. def OAI.Kadison.HilbertTensor.insertRight line 34
  5. lemma OAI.Kadison.HilbertTensor.insertRight_apply line 37
  6. lemma OAI.Kadison.HilbertTensor.norm_insertRight_le line 39
  7. def OAI.Kadison.HilbertTensor.insertLeft line 44
  8. lemma OAI.Kadison.HilbertTensor.insertLeft_apply line 47
  9. lemma OAI.Kadison.HilbertTensor.norm_insertLeft_le line 49
  10. lemma OAI.Kadison.HilbertTensor.insertRight_adjoint_pair line 54
  11. lemma OAI.Kadison.HilbertTensor.insertLeft_adjoint_pair line 61
  12. def OAI.Kadison.HilbertTensor.scalarSlice line 67
  13. lemma OAI.Kadison.HilbertTensor.scalarSlice_inner line 71
  14. lemma OAI.Kadison.HilbertTensor.eq_zero_of_pair_inner line 77
  15. lemma OAI.Kadison.HilbertTensor.pair_inner_ext line 89
  16. lemma OAI.Kadison.HilbertTensor.eq_zero_of_scalarSlice line 96