OAI/Analysis/Commutator/TensorDevelopment.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.HilbertTensor.slicePre line 21
  2. lemma OAI.Kadison.HilbertTensor.slicePre_tmul line 25
  3. lemma OAI.Kadison.HilbertTensor.norm_slicePre_le line 28
  4. def OAI.Kadison.HilbertTensor.slice line 43
  5. lemma OAI.Kadison.HilbertTensor.slice_coe line 46
  6. lemma OAI.Kadison.HilbertTensor.norm_slice_le line 50
  7. lemma OAI.Kadison.HilbertTensor.tendsto_slice_zero line 59
  8. lemma OAI.Kadison.HilbertTensor.tendsto_orthonormal_inner_zero line 80
  9. lemma OAI.Kadison.HilbertTensor.norm_completion line 87
  10. lemma OAI.Kadison.HilbertTensor.norm_mapL line 102
  11. def OAI.Kadison.HilbertTensor.map line 123
  12. lemma OAI.Kadison.HilbertTensor.norm_map line 127
  13. lemma OAI.Kadison.HilbertTensor.map_coe_tmul line 130
  14. lemma OAI.Kadison.HilbertTensor.completion_ext line 135
  15. lemma OAI.Kadison.HilbertTensor.map_add_left line 146
  16. lemma OAI.Kadison.HilbertTensor.map_add_right line 152
  17. lemma OAI.Kadison.HilbertTensor.map_sub_right line 158
  18. lemma OAI.Kadison.HilbertTensor.map_smul_left line 164
  19. lemma OAI.Kadison.HilbertTensor.map_smul_right line 170
  20. lemma OAI.Kadison.HilbertTensor.map_mul line 176
  21. lemma OAI.Kadison.HilbertTensor.map_one_one line 182
  22. lemma OAI.Kadison.HilbertTensor.hankel_commutator_norm line 187
  23. lemma OAI.Kadison.HilbertTensor.tendsto_orthonormal_slice_zero line 199