OAI/Computability/MaxCut/Games/MatrixCharacters.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Trace characters on actual finite binary matrix spaces.

  1. abbrev OAI.MaxCutGames.Fourier.MatrixCharacters.F2 line 15
  2. def OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair line 18

    Source documentation

    The binary trace pairing between oppositely oriented matrices.

    def tracePair {n m : Nat} (X : Matrix (Fin n) (Fin m) F2)
    (S : Matrix (Fin m) (Fin n) F2) : F2 := Matrix.trace (X * S)

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2

  3. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_eq_sum_entries line 21
  4. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_swap line 25
  5. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_zero_left line 29
  6. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_zero_right line 32
  7. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_add_left line 35
  8. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_add_right line 40
  9. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_ext_right line 45
  10. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair_ext_left line 49
  11. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.exists_tracePair_eq_one line 54

    Source documentation

    A nonzero matrix has trace pairing one with a dual matrix.

    theorem exists_tracePair_eq_one {n m : Nat} (S : Matrix (Fin m) (Fin n) F2)
    (hS : S ≠ 0) : ∃ X, tracePair X S = 1 := by
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2, OAI.MaxCutGames.Fourier.MatrixCharacters.tracePair

  12. def OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign line 66

    Source documentation

    The unique nontrivial complex-valued character of the binary field.

    def binarySign (a : F2) : ℂ := if a = 0 then 1 else -1

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2

  13. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_zero line 68
  14. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_one line 69
  15. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_eq_neg_one_pow_val line 71
  16. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_add line 76
  17. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_sum line 81
  18. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_injective line 88
  19. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_real line 99
  20. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_im line 103
  21. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.binarySign_mul_self line 107
  22. def OAI.MaxCutGames.Fourier.MatrixCharacters.linearFunctionalCharacter line 116

    Source documentation

    A binary linear functional determines a complex additive character.

    def linearFunctionalCharacter (φ : E →ₗ[F2] F2) : AddChar E ℂ where
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2

  23. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearFunctionalCharacter_apply line 121
  24. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearFunctionalCharacter_zero line 124
  25. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearFunctionalCharacter_injective line 129
  26. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearFunctionalCharacter_eq_zero_iff line 136
  27. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.sum_linearFunctionalCharacter line 140
  28. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.expect_linearFunctionalCharacter line 146
  29. def OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter line 153
  30. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_apply line 159
  31. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_eq_coordinate_sign line 163
  32. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_eq_trace_exponent line 167
  33. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_eq_product_entries line 172
  34. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_real line 177
  35. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_add line 181
  36. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_zero line 186
  37. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_injective line 191
  38. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.traceCharacter_eq_zero_iff line 199
  39. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.sum_traceCharacter line 203
  40. def OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair line 214

    Source documentation

    The basis-independent trace pairing in the statement of Lemma 2.1.

    def linearTracePair (X : E →ₗ[F2] F) (S : F →ₗ[F2] E) : F2 :=
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2

  41. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_eq_matrix_tracePair line 217
  42. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_zero_left line 226
  43. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_zero_right line 229
  44. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_add_left line 232
  45. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_add_right line 236
  46. def OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter line 241

    Source documentation

    The trace character on actual linear maps, with no choice of basis.

    def linearTraceCharacter (S : F →ₗ[F2] E) : AddChar (E →ₗ[F2] F) ℂ where
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2

  47. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_apply line 246
  48. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_real line 249
  49. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_add line 252
  50. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_zero line 258
  51. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_eq_matrix_traceCharacter line 263
  52. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_swap line 273
  53. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_swap line 277
  54. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_ext_right line 282

    Source documentation

    The actual trace pairing is nondegenerate in its dual-map argument.

    theorem linearTracePair_ext_right {S T : F →ₗ[F2] E}
    (h : ∀ X, linearTracePair X S = linearTracePair X T) : S = T := by
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2, OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair

  55. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair_ext_left line 295

    Source documentation

    Nondegeneracy also holds in the primal-map argument.

    theorem linearTracePair_ext_left {X Y : E →ₗ[F2] F}
    (h : ∀ S, linearTracePair X S = linearTracePair Y S) : X = Y := by
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixCharacters.F2, OAI.MaxCutGames.Fourier.MatrixCharacters.linearTracePair

  56. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.exists_linearTracePair_eq_one line 307
  57. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_injective line 318
  58. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.linearTraceCharacter_eq_zero_iff line 326
  59. theorem OAI.MaxCutGames.Fourier.MatrixCharacters.sum_linearTraceCharacter line 330