OAI/Analysis/Commutator/HankelAlgebra.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Kadison.FreeMoments.free_of_different_endpoints line 22
  2. lemma OAI.Kadison.FreeMoments.product_vanish_on_spans line 76
  3. lemma OAI.Kadison.FreeMoments.letterList_of_values line 98
  4. theorem OAI.Kadison.FreeMoments.free_of_spanning_alphabets line 107
  5. def OAI.Kadison.FreeMoments.paired line 131
  6. lemma OAI.Kadison.FreeMoments.paired_nil line 134
  7. lemma OAI.Kadison.FreeMoments.paired_cons line 136
  8. lemma OAI.Kadison.FreeMoments.paired_append line 139
  9. lemma OAI.Kadison.FreeMoments.paired_reduced line 142
  10. lemma OAI.Kadison.FreeMoments.paired_moment line 152
  11. lemma OAI.Kadison.FreeMoments.word_paired_replicate line 159
  12. def OAI.Kadison.FreeMoments.dihedralBlocks line 165
  13. lemma OAI.Kadison.FreeMoments.word_dihedralBlocks line 168
  14. theorem OAI.Kadison.FreeMoments.dihedral_cyclic_moment line 180
  15. lemma OAI.Kadison.CornerMoments.left_support_prod line 213
  16. lemma OAI.Kadison.CornerMoments.compressed_prod line 221
  17. lemma OAI.Kadison.CornerMoments.traceremove line 235
  18. def OAI.Kadison.DihedralCorner.wave line 250
  19. lemma OAI.Kadison.DihedralCorner.wave_zero line 252
  20. lemma OAI.Kadison.DihedralCorner.wave_add line 254
  21. lemma OAI.Kadison.DihedralCorner.wave_star line 257
  22. lemma OAI.Kadison.DihedralCorner.reflection_wave line 263
  23. def OAI.Kadison.DihedralCorner.cosine line 274
  24. lemma OAI.Kadison.DihedralCorner.cosine_coe line 277
  25. lemma OAI.Kadison.DihedralCorner.cosine_zero line 279
  26. lemma OAI.Kadison.DihedralCorner.cosine_star line 283
  27. lemma OAI.Kadison.DihedralCorner.cosine_neg line 291
  28. lemma OAI.Kadison.DihedralCorner.cosine_mul line 300
  29. def OAI.Kadison.DihedralCorner.cosineSpace line 335
  30. lemma OAI.Kadison.DihedralCorner.cosine_mem line 337
  31. lemma OAI.Kadison.DihedralCorner.cosineSpace_mul line 341
  32. lemma OAI.Kadison.DihedralCorner.cosineSpace_star line 359
  33. def OAI.Kadison.DihedralCorner.cosineAlgebra line 366
  34. def OAI.Kadison.DihedralCorner.positiveCosines line 377
  35. lemma OAI.Kadison.DihedralCorner.cosine_nonzero_mem_positive line 380
  36. lemma OAI.Kadison.DihedralCorner.center_cosineSpace line 399
  37. lemma OAI.Kadison.DihedralCorner.centered_cosineAlgebra_span line 419
  38. lemma OAI.Kadison.FreeMoments.alternating_power_centered line 434
  39. lemma OAI.Kadison.FreeMoments.alternating_odd_centered line 441
  40. lemma OAI.Kadison.DihedralCorner.cosine_positive_centered line 469
  41. def OAI.Kadison.cornerFactor line 494
  42. lemma OAI.Kadison.corner_list_prod_coe line 514
  43. def OAI.Kadison.halfCornerTrace line 524
  44. lemma OAI.Kadison.halfCornerTrace_apply line 527
  45. lemma OAI.Kadison.halfCornerTrace_tracial line 530
  46. lemma OAI.Kadison.halfCornerTrace_star line 535
  47. theorem OAI.Kadison.DihedralCorner.corner_cosine_pair_moment line 561
  48. def OAI.Kadison.FreeMoments.flattenPairs line 623
  49. lemma OAI.Kadison.FreeMoments.flattenPairs_nil line 626
  50. lemma OAI.Kadison.FreeMoments.flattenPairs_cons line 628
  51. lemma OAI.Kadison.FreeMoments.word_flattenPairs line 631
  52. lemma OAI.Kadison.FreeMoments.flattenPairs_parse line 638
  53. theorem OAI.Kadison.FreeMoments.free_bool_of_pair_moments line 670
  54. lemma OAI.Kadison.FreeMoments.paired_vanish_on_spans line 697
  55. lemma OAI.Kadison.FreeMoments.pair_generators_witness line 723
  56. lemma OAI.Kadison.FreeMoments.zipWith_same_maps line 733
  57. lemma OAI.Kadison.FreeMoments.pairs_vanish_on_second_span line 741
  58. lemma OAI.Kadison.DihedralCorner.halfCornerTrace_one line 789
  59. lemma OAI.Kadison.DihedralCorner.cosine_centered line 794
  60. def OAI.Kadison.DihedralCorner.cornerPairFactors line 808
  61. theorem OAI.Kadison.DihedralCorner.corner_cosine_free line 812