OAI/Analysis/Commutator/FiniteTestPatching.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FiniteTest.sign line 19
  2. lemma OAI.Kadison.FiniteTest.sign_not line 21
  3. lemma OAI.Kadison.FiniteTest.sign_sq line 23
  4. def OAI.Kadison.FiniteTest.flip line 25
  5. lemma OAI.Kadison.FiniteTest.flip_involutive line 27
  6. def OAI.Kadison.FiniteTest.flipEquiv line 34
  7. def OAI.Kadison.FiniteTest.character line 36
  8. lemma OAI.Kadison.FiniteTest.character_empty line 39
  9. lemma OAI.Kadison.FiniteTest.character_sq line 42
  10. lemma OAI.Kadison.FiniteTest.character_flip line 46
  11. lemma OAI.Kadison.FiniteTest.character_sum_zero line 65
  12. lemma OAI.Kadison.FiniteTest.different_character_sum line 73
  13. lemma OAI.Kadison.FiniteTest.character_gram line 92
  14. lemma OAI.Kadison.FiniteTest.sign_parseval line 108
  15. abbrev OAI.Kadison.FiniteTest.Upper line 141
  16. def OAI.Kadison.FiniteTest.label line 143
  17. lemma OAI.Kadison.FiniteTest.label_injective line 148
  18. lemma OAI.Kadison.FiniteTest.sum_upper line 194
  19. lemma OAI.Kadison.FiniteTest.sum_matrix_split line 199
  20. def OAI.Kadison.FiniteTest.matrixSignSum line 231
  21. def OAI.Kadison.FiniteTest.matrixCoefficient line 234
  22. lemma OAI.Kadison.FiniteTest.matrixSignSum_eq line 238
  23. lemma OAI.Kadison.FiniteTest.norm_add_sq_bound line 250
  24. lemma OAI.Kadison.FiniteTest.upper_norm_sum_bound line 255
  25. theorem OAI.Kadison.FiniteTest.exists_matrix_sign_bound line 268
  26. def OAI.Kadison.FiniteTest.unit line 293
  27. lemma OAI.Kadison.FiniteTest.unit_star line 295
  28. lemma OAI.Kadison.FiniteTest.unit_mul line 298
  29. lemma OAI.Kadison.FiniteTest.unit_sum line 304
  30. def OAI.Kadison.FiniteTest.column line 307
  31. lemma OAI.Kadison.FiniteTest.star_column line 309
  32. lemma OAI.Kadison.FiniteTest.column_right line 313
  33. lemma OAI.Kadison.FiniteTest.column_inner line 317
  34. lemma OAI.Kadison.FiniteTest.column_sandwich line 332
  35. def OAI.Kadison.FiniteTest.traceSquare line 345
  36. lemma OAI.Kadison.FiniteTest.traceSquare_smul line 347
  37. lemma OAI.Kadison.FiniteTest.trace_rotate line 355
  38. lemma OAI.Kadison.FiniteTest.unit_trace_eq line 359
  39. lemma OAI.Kadison.FiniteTest.unit_trace line 363
  40. def OAI.Kadison.FiniteTest.signProjection line 376
  41. lemma OAI.Kadison.FiniteTest.signProjection_star line 379
  42. lemma OAI.Kadison.FiniteTest.signProjection_idem line 383
  43. lemma OAI.Kadison.FiniteTest.isStarProjection_signProjection line 396
  44. lemma OAI.Kadison.FiniteTest.signProjection_trace line 401
  45. lemma OAI.Kadison.FiniteTest.block_traceSquare line 410
  46. lemma OAI.Kadison.FiniteTest.sum_block_traceSquare line 421
  47. lemma OAI.Kadison.FiniteTest.column_left_star line 428
  48. lemma OAI.Kadison.FiniteTest.column_compression_left line 432
  49. lemma OAI.Kadison.FiniteTest.column_compression_right line 437
  50. lemma OAI.Kadison.FiniteTest.column_outer_traceSquare line 443
  51. lemma OAI.Kadison.FiniteTest.signProjection_compression_traceSquare line 460
  52. def OAI.Kadison.FiniteTest.expectation line 476
  53. lemma OAI.Kadison.FiniteTest.expectation_left line 479
  54. lemma OAI.Kadison.FiniteTest.expectation_right line 490
  55. lemma OAI.Kadison.FiniteTest.expectation_commutes line 501
  56. lemma OAI.Kadison.FiniteTest.expectation_star line 505
  57. lemma OAI.Kadison.FiniteTest.unit_mul_trace line 510
  58. lemma OAI.Kadison.FiniteTest.expectation_star_commutes line 528
  59. lemma OAI.Kadison.FiniteTest.diagonal_traceSquare line 534
  60. lemma OAI.Kadison.FiniteTest.matrixSignSum_vector line 569
  61. theorem OAI.Kadison.FiniteTest.exists_signProjection_bound line 576
  62. def OAI.Kadison.FiniteTest.familyVector line 609
  63. lemma OAI.Kadison.FiniteTest.familyVector_apply line 614
  64. def OAI.Kadison.FiniteTest.familyTrace line 617
  65. lemma OAI.Kadison.FiniteTest.familyTrace_apply line 619
  66. lemma OAI.Kadison.FiniteTest.familyTrace_tracial line 623
  67. lemma OAI.Kadison.FiniteTest.familyVector_norm_sq line 628
  68. def OAI.Kadison.FiniteTest.familyHom line 634
  69. lemma OAI.Kadison.FiniteTest.familyHom_apply line 638
  70. lemma OAI.Kadison.FiniteTest.unit_family line 640
  71. lemma OAI.Kadison.FiniteTest.column_family line 642
  72. lemma OAI.Kadison.FiniteTest.signProjection_family line 646
  73. lemma OAI.Kadison.FiniteTest.expectation_family line 650
  74. theorem OAI.Kadison.FiniteTest.exists_signProjection_family_bound line 655
  75. def OAI.Kadison.FiniteTest.realTrace line 679
  76. lemma OAI.Kadison.FiniteTest.realTrace_apply line 683
  77. def OAI.Kadison.FiniteTest.vector line 685
  78. lemma OAI.Kadison.FiniteTest.vector_apply line 689
  79. lemma OAI.Kadison.FiniteTest.vector_norm_sq line 691
  80. lemma OAI.Kadison.FiniteTest.real_smul_mem_range line 700
  81. lemma OAI.Kadison.FiniteTest.signProjection_mem_range line 705
  82. theorem OAI.Kadison.FiniteTest.exists_rankOne_finite_test line 713