OAI/Computability/DirectedFeedback/Analysis/MatrixCharacters.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Fourier.MatrixCharacters.F2 line 13
  2. def OAI.DFVSGames.Fourier.MatrixCharacters.tracePair line 15
  3. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_eq_sum_entries line 18
  4. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_swap line 22
  5. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_zero_left line 26
  6. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_zero_right line 29
  7. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_add_left line 32
  8. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_add_right line 37
  9. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_ext_right line 42
  10. theorem OAI.DFVSGames.Fourier.MatrixCharacters.tracePair_ext_left line 46
  11. theorem OAI.DFVSGames.Fourier.MatrixCharacters.exists_tracePair_eq_one line 50
  12. def OAI.DFVSGames.Fourier.MatrixCharacters.binarySign line 61
  13. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_zero line 63
  14. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_one line 64
  15. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_eq_neg_one_pow_val line 66
  16. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_add line 71
  17. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_sum line 76
  18. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_injective line 83
  19. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_real line 94
  20. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_im line 98
  21. theorem OAI.DFVSGames.Fourier.MatrixCharacters.binarySign_mul_self line 102
  22. def OAI.DFVSGames.Fourier.MatrixCharacters.linearFunctionalCharacter line 110
  23. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearFunctionalCharacter_apply line 115
  24. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearFunctionalCharacter_zero line 118
  25. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearFunctionalCharacter_injective line 123
  26. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearFunctionalCharacter_eq_zero_iff line 130
  27. theorem OAI.DFVSGames.Fourier.MatrixCharacters.sum_linearFunctionalCharacter line 134
  28. theorem OAI.DFVSGames.Fourier.MatrixCharacters.expect_linearFunctionalCharacter line 140
  29. def OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter line 147
  30. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_apply line 153
  31. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_eq_coordinate_sign line 157
  32. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_eq_trace_exponent line 161
  33. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_eq_product_entries line 166
  34. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_real line 171
  35. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_add line 175
  36. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_zero line 180
  37. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_injective line 185
  38. theorem OAI.DFVSGames.Fourier.MatrixCharacters.traceCharacter_eq_zero_iff line 193
  39. theorem OAI.DFVSGames.Fourier.MatrixCharacters.sum_traceCharacter line 197
  40. def OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair line 207
  41. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_eq_matrix_tracePair line 210
  42. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_zero_left line 219
  43. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_zero_right line 222
  44. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_add_left line 225
  45. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_add_right line 229
  46. def OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter line 233
  47. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_apply line 238
  48. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_real line 241
  49. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_add line 244
  50. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_zero line 250
  51. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_eq_matrix_traceCharacter line 255
  52. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_swap line 265
  53. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_swap line 269
  54. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_ext_right line 273
  55. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTracePair_ext_left line 285
  56. theorem OAI.DFVSGames.Fourier.MatrixCharacters.exists_linearTracePair_eq_one line 297
  57. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_injective line 308
  58. theorem OAI.DFVSGames.Fourier.MatrixCharacters.linearTraceCharacter_eq_zero_iff line 316
  59. theorem OAI.DFVSGames.Fourier.MatrixCharacters.sum_linearTraceCharacter line 320
  60. theorem OAI.DFVSGames.Fourier.MatrixParity.trace_rankOne line 337
  61. def OAI.DFVSGames.Fourier.MatrixParity.MatrixValid line 343
  62. theorem OAI.DFVSGames.Fourier.MatrixParity.matrixValid_iff_exists line 346
  63. theorem OAI.DFVSGames.Fourier.MatrixParity.exists_matrixValid line 364
  64. theorem OAI.DFVSGames.Fourier.MatrixParity.comp_ne_zero_iff_exists line 383
  65. def OAI.DFVSGames.Fourier.MatrixParity.Valid line 407
  66. theorem OAI.DFVSGames.Fourier.MatrixParity.valid_iff_exists line 409
  67. theorem OAI.DFVSGames.Fourier.MatrixParity.exists_valid line 412
  68. theorem OAI.DFVSGames.Fourier.MatrixParity.trace_smulRight_comp line 428
  69. theorem OAI.DFVSGames.Fourier.MatrixParity.card_linearMaps line 436
  70. theorem OAI.DFVSGames.Fourier.MatrixParity.card_linearMaps_le line 450
  71. theorem OAI.DFVSGames.Fourier.MatrixParity.folded_indicator_sum_le_one line 468
  72. theorem OAI.DFVSGames.Fourier.MatrixParity.folded_indicator_average_le line 490
  73. def OAI.DFVSGames.Fourier.MatrixParity.parityCharacter line 508
  74. theorem OAI.DFVSGames.Fourier.MatrixParity.parityCharacter_eq_zero_iff line 513
  75. theorem OAI.DFVSGames.Fourier.MatrixParity.linearTrace_shift_sum line 527
  76. theorem OAI.DFVSGames.Fourier.MatrixParity.linearTrace_shift_average line 537
  77. def OAI.DFVSGames.Fourier.MatrixFourier.fourierCoeff line 562
  78. theorem OAI.DFVSGames.Fourier.MatrixFourier.fourierCoeff_sum line 565
  79. theorem OAI.DFVSGames.Fourier.MatrixFourier.fourierCoeff_smul line 571
  80. theorem OAI.DFVSGames.Fourier.MatrixFourier.star_expect line 577
  81. theorem OAI.DFVSGames.Fourier.MatrixFourier.star_fourierCoeff line 581
  82. def OAI.DFVSGames.Fourier.MatrixFourier.linearCoeff line 593
  83. theorem OAI.DFVSGames.Fourier.MatrixFourier.card_linearMap_reverse line 596
  84. theorem OAI.DFVSGames.Fourier.MatrixFourier.linearTraceCharacter_star line 618
  85. theorem OAI.DFVSGames.Fourier.MatrixFourier.linearMap_add_eq_zero_iff line 628
  86. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_character_kernel line 637
  87. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_complexCoeff_character line 655
  88. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_complex_inversion line 667
  89. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_complex_parseval line 678
  90. theorem OAI.DFVSGames.Fourier.MatrixFourier.complex_ofReal_expect line 696
  91. theorem OAI.DFVSGames.Fourier.MatrixFourier.linearCoeff_complex line 703
  92. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_parseval_inner line 711
  93. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_parseval line 731
  94. theorem OAI.DFVSGames.Fourier.MatrixFourier.linear_fourier_inversion line 735
  95. theorem OAI.DFVSGames.Fourier.MatrixFourier.linearCoeff_sum line 753
  96. theorem OAI.DFVSGames.Fourier.MatrixFourier.linearCoeff_smul line 760
  97. theorem OAI.DFVSGames.Fourier.MatrixFourier.linearCoeff_character line 766