OAI/Analysis/Commutator/FreeMoments.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Kadison.FreeMoments.Letter line 24
  2. def OAI.Kadison.FreeMoments.word line 32
  3. def OAI.Kadison.FreeMoments.Reduced line 34
  4. def OAI.Kadison.FreeMoments.Free line 37
  5. lemma OAI.Kadison.FreeMoments.word_nil line 40
  6. lemma OAI.Kadison.FreeMoments.word_cons line 42
  7. lemma OAI.Kadison.FreeMoments.word_append line 45
  8. lemma OAI.Kadison.FreeMoments.reduced_nil line 48
  9. lemma OAI.Kadison.FreeMoments.reduced_singleton line 50
  10. lemma OAI.Kadison.FreeMoments.Reduced.tail line 52
  11. def OAI.Kadison.FreeMoments.Letter.conj line 57
  12. lemma OAI.Kadison.FreeMoments.star_color line 63
  13. lemma OAI.Kadison.FreeMoments.star_val line 65
  14. def OAI.Kadison.FreeMoments.reverseStar line 67
  15. lemma OAI.Kadison.FreeMoments.word_reverseStar line 70
  16. lemma OAI.Kadison.FreeMoments.Reduced.reverseStar line 79
  17. lemma OAI.Kadison.FreeMoments.reduced_join line 85
  18. lemma OAI.Kadison.FreeMoments.gram_different_head line 98
  19. def OAI.Kadison.FreeMoments.centeredPair line 108
  20. lemma OAI.Kadison.FreeMoments.reduced_pair_join line 116
  21. lemma OAI.Kadison.FreeMoments.gram_same_head line 136
  22. def OAI.Kadison.FreeMoments.gram line 152
  23. theorem OAI.Kadison.FreeMoments.gram_word line 159
  24. lemma OAI.Kadison.FreeMoments.gram_zero_of_colors_ne line 179
  25. lemma OAI.Kadison.FreeMoments.gram_ofFn line 195
  26. lemma OAI.Kadison.FreeMoments.reduced_word_orthogonal line 205
  27. lemma OAI.Kadison.FreeMoments.reduced_word_inner line 211
  28. def OAI.Kadison.FreeMoments.centerLetter line 218
  29. def OAI.Kadison.FreeMoments.wordSpan line 224
  30. lemma OAI.Kadison.FreeMoments.word_mem_span line 227
  31. lemma OAI.Kadison.FreeMoments.one_mem_wordSpan line 230
  32. lemma OAI.Kadison.FreeMoments.generator_mem_wordSpan line 234
  33. lemma OAI.Kadison.FreeMoments.generator_mul_word line 243
  34. lemma OAI.Kadison.FreeMoments.generator_mul_span line 272
  35. lemma OAI.Kadison.FreeMoments.word_mul_span line 283
  36. lemma OAI.Kadison.FreeMoments.mul_mem_wordSpan line 291
  37. lemma OAI.Kadison.FreeMoments.star_mem_wordSpan line 302
  38. def OAI.Kadison.FreeMoments.reducedAlgebra line 314
  39. lemma OAI.Kadison.FreeMoments.generator_le_reducedAlgebra line 327
  40. lemma OAI.Kadison.FreeMoments.reducedAlgebra_eq_iSup line 330