OAI/Computability/UniqueGames/Analysis/MatrixCharactersLemmas.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

Trace characters on actual finite binary matrix spaces.

  1. abbrev OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.F2 line 25
  2. def OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair line 28

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2

  3. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_eq_sum_entries line 31
  4. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_swap line 35
  5. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_zero_left line 39
  6. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_zero_right line 42
  7. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_add_left line 45
  8. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_add_right line 50
  9. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_ext_right line 55
  10. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair_ext_left line 59
  11. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.exists_tracePair_eq_one line 64

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2, OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.tracePair

  12. def OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign line 76

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2

  13. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_zero line 78
  14. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_one line 79
  15. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_eq_neg_one_pow_val line 81
  16. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_add line 86
  17. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_sum line 91
  18. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_injective line 98
  19. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_real line 109
  20. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_im line 113
  21. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.binarySign_mul_self line 117
  22. def OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearFunctionalCharacter line 126

    Source documentation

    A binary linear functional determines a complex additive character.

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

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.F2

  23. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearFunctionalCharacter_apply line 131
  24. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearFunctionalCharacter_zero line 134
  25. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearFunctionalCharacter_injective line 139
  26. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearFunctionalCharacter_eq_zero_iff line 146
  27. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.sum_linearFunctionalCharacter line 150
  28. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.expect_linearFunctionalCharacter line 156
  29. def OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter line 163
  30. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_apply line 169
  31. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_eq_coordinate_sign line 173
  32. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_eq_trace_exponent line 177
  33. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_eq_product_entries line 182
  34. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_real line 187
  35. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_add line 191
  36. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_zero line 196
  37. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_injective line 201
  38. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.traceCharacter_eq_zero_iff line 209
  39. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.sum_traceCharacter line 213
  40. def OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair line 226

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2

  41. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_eq_matrix_tracePair line 229
  42. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_zero_left line 238
  43. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_zero_right line 241
  44. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_add_left line 244
  45. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_add_right line 248
  46. def OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter line 253

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2

  47. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_apply line 258
  48. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_real line 261
  49. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_add line 264
  50. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_zero line 270
  51. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_eq_matrix_traceCharacter line 275
  52. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_swap line 285
  53. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_swap line 289
  54. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_ext_right line 294

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2, OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair

  55. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair_ext_left line 307

    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.UniqueGamesTheorem.Fourier.MatrixCharacters.F2, OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTracePair

  56. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.exists_linearTracePair_eq_one line 319
  57. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_injective line 330
  58. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.linearTraceCharacter_eq_zero_iff line 338
  59. theorem OAI.UniqueGamesTheorem.Fourier.MatrixCharacters.sum_linearTraceCharacter line 342
  60. def OAI.UniqueGamesTheorem.Fourier.MatrixFourier.fourierCoeff line 383

    Source documentation

    Uniformly normalized complex Fourier coefficient.

    def fourierCoeff (f : G → ℂ) (ψ : AddChar G ℂ) : ℂ :=
…
  61. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.fourierCoeff_sum line 386
  62. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.fourierCoeff_smul line 392
  63. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.star_expect line 398
  64. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.star_fourierCoeff line 402
  65. def OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff line 417

    Source documentation

    Real coefficient on the actual space of binary linear maps.

    def linearCoeff (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) : ℝ :=
…
  66. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.card_linearMap_reverse line 420
  67. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearTraceCharacter_star line 442
  68. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearMap_add_eq_zero_iff line 452
  69. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_character_kernel line 462

    Source documentation

    Exact trace-character orthogonality with the frequency sum unnormalized.

    theorem linear_character_kernel (X Y : E →ₗ[F2] F) :
    ∑ S : F →ₗ[F2] E, star (linearTraceCharacter S X) * linearTraceCharacter S Y =
      if X = Y then (Fintype.card (E →ₗ[F2] F) : ℂ) else 0 := by
…
  70. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_complexCoeff_character line 480
  71. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_complex_inversion line 493

    Source documentation

    Fourier inversion obtained directly from the finite trace orthogonality sum.

    theorem linear_complex_inversion (f : (E →ₗ[F2] F) → ℂ) (Y : E →ₗ[F2] F) :
    ∑ S : F →ₗ[F2] E, fourierCoeff f (linearTraceCharacter S) *
      linearTraceCharacter S Y = f Y := by
…

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixFourier.fourierCoeff

  72. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_complex_parseval line 505

    Source documentation

    Mixed Parseval with normalized primal expectation and unnormalized frequency sum.

    theorem linear_complex_parseval (f g : (E →ₗ[F2] F) → ℂ) :
    ∑ S : F →ₗ[F2] E, star (fourierCoeff f (linearTraceCharacter S)) *
      fourierCoeff g (linearTraceCharacter S) = 𝔼 X, star (f X) * g X := by
…

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixFourier.fourierCoeff

  73. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.complex_ofReal_expect line 523
  74. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff_complex line 530
  75. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_parseval_inner line 539

    Source documentation

    Parseval for real functions and the real binary trace coefficients.

    theorem linear_parseval_inner (f g : (E →ₗ[F2] F) → ℝ) :
    ∑ S : F →ₗ[F2] E, linearCoeff f S * linearCoeff g S =
      𝔼 X, f X * g X := by
…

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff

  76. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_parseval line 559
  77. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linear_fourier_inversion line 563
  78. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff_sum line 581
  79. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff_smul line 588
  80. theorem OAI.UniqueGamesTheorem.Fourier.MatrixFourier.linearCoeff_character line 594
  81. theorem OAI.UniqueGamesTheorem.Appendix.DegreeZero.rank_pos_of_ne_zero line 624
  82. theorem OAI.UniqueGamesTheorem.Appendix.DegreeZero.eq_constant_of_degree_zero line 637
  83. theorem OAI.UniqueGamesTheorem.Appendix.DegreeZero.fourth_moment_eq_energy_sq line 647
  84. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.trace_rankOne line 672

    Source documentation

    The rank-one shift c τ paired against S evaluates the functional τ S at c, exactly the parity appearing in the decoding condition.

    theorem trace_rankOne {m n : Nat} (c : Vector n) (τ : Vector m)
    (S : Matrix (Fin m) (Fin n) F2) :
    Matrix.trace (Matrix.vecMulVec c τ * S) = τ ⬝ᵥ (S *ᵥ c) := by
…
  85. def OAI.UniqueGamesTheorem.Fourier.MatrixParity.MatrixValid line 679

    Source documentation

    Coordinate form of the requirement τ ∘ T ≠ 0.

    def MatrixValid {m n : Nat} (τ : Vector m) (S : Matrix (Fin m) (Fin n) F2) : Prop :=
…
  86. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.matrixValid_iff_exists line 682
  87. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.exists_matrixValid line 700
  88. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.comp_ne_zero_iff_exists line 720

    Source documentation

    Abstract linear-map form of the nonzero-parity condition.

    theorem comp_ne_zero_iff_exists {E C : Type*}
    [AddCommGroup E] [Module F2 E] [AddCommGroup C] [Module F2 C]
    (τ : E →ₗ[F2] F2) (T : C →ₗ[F2] E) :
    τ.comp T ≠ 0 ↔ ∃ c, τ (T c) = 1 := by
…
  89. def OAI.UniqueGamesTheorem.Fourier.MatrixParity.Valid line 744
  90. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.valid_iff_exists line 746
  91. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.exists_valid line 751

    Source documentation

    Any nonzero parity functional admits a parity-valid map out of a nontrivial binary vector space. This also proves the candidate family is nonempty.

    theorem exists_valid [Nontrivial C] (τ : E →ₗ[F2] F2) (hτ : τ ≠ 0) :
    ∃ S : C →ₗ[F2] E, Valid τ S := by
…

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixParity.Valid

  92. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.trace_smulRight_comp line 768

    Source documentation

    Generic trace pairing of a rank-one color shift.

    theorem trace_smulRight_comp [FiniteDimensional F2 C]
    (τ : E →ₗ[F2] F2) (c : C) (S : C →ₗ[F2] E) :
    LinearMap.trace F2 C ((τ.smulRight c).comp S) = τ (S c) := by
…
  93. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.card_linearMaps line 778

    Source documentation

    The exact number of binary linear maps, supplying the count in (5.20). Taking E to be the subspace W counts precisely maps whose image lies in W.

    theorem card_linearMaps [FiniteDimensional F2 E] [FiniteDimensional F2 C]
    [Fintype (C →ₗ[F2] E)] :
    Fintype.card (C →ₗ[F2] E) =
      2 ^ (Module.finrank F2 C * Module.finrank F2 E) := by
…
  94. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.card_linearMaps_le line 792
  95. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.folded_indicator_sum_le_one line 812

    Source documentation

    A folded map hits a fixed color at most once along its C-shift orbit. The injection models the inclusion of the subspace C' in the full color space.

    theorem folded_indicator_sum_le_one (τ : E →ₗ[F2] F2)
    (inclusion : C →ₗ[F2] D) (inclusion_injective : Function.Injective inclusion)
    (F : (E →ₗ[F2] C) → D)
    (folded : ∀ X c, F (X + τ.smulRight c) = F X + inclusion c)
    (X : E →ₗ[F2] C) (y : D) :
    (∑ c : C, if F (X + τ.smulRight c) = y then (1 : ℝ) else 0) ≤ 1 := by
…
  96. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.folded_indicator_average_le line 835

    Source documentation

    Equation (5.19)'s first bound, with the actual finite folded shift average.

    theorem folded_indicator_average_le (τ : E →ₗ[F2] F2)
    (inclusion : C →ₗ[F2] D) (inclusion_injective : Function.Injective inclusion)
    (F : (E →ₗ[F2] C) → D)
    (folded : ∀ X c, F (X + τ.smulRight c) = F X + inclusion c)
    (X : E →ₗ[F2] C) (y : D) :
    (∑ c : C, if F (X + τ.smulRight c) = y then (1 : ℝ) else 0) /
        Fintype.card C ≤ 1 / (Fintype.card C : ℝ) := by
…
  97. def OAI.UniqueGamesTheorem.Fourier.MatrixParity.parityCharacter line 856

    Source documentation

    The character of the color-shift group indexed by the functional τ S.

    def parityCharacter (τ : E →ₗ[F2] F2) (S : C →ₗ[F2] E) : AddChar C ℂ where
…
  98. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.parityCharacter_eq_zero_iff line 861
  99. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.linearTrace_shift_sum line 876

    Source documentation

    Unnormalized annihilator identity for exactly the c τ shift subgroup.

    theorem linearTrace_shift_sum [Fintype C] [FiniteDimensional F2 C]
    (τ : E →ₗ[F2] F2) (S : C →ₗ[F2] E) :
    (∑ c : C, linearTraceCharacter S (τ.smulRight c)) =
      if τ.comp S = 0 then (Fintype.card C : ℂ) else 0 := by
…
  100. theorem OAI.UniqueGamesTheorem.Fourier.MatrixParity.linearTrace_shift_average line 888

    Source documentation

    Averaging the Fourier character in the folding directions kills precisely the indices with nonzero τ S, the multiplier used in Equation (5.19).

    theorem linearTrace_shift_average [Fintype C] [FiniteDimensional F2 C]
    (τ : E →ₗ[F2] F2) (S : C →ₗ[F2] E) :
    (∑ c : C, linearTraceCharacter S (τ.smulRight c)) / (Fintype.card C : ℂ) =
      if τ.comp S = 0 then 1 else 0 := by
…