OAI/LinearAlgebra/Hadamard/Fourier.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Fourier identities and the entrywise square of a Hadamard matrix.

  1. lemma OAI.HadamardSix.alpha_balanced line 11
  2. lemma OAI.HadamardSix.Balanced.permute line 14
  3. lemma OAI.HadamardSix.character_zero line 20
  4. lemma OAI.HadamardSix.character_add line 23
  5. lemma OAI.HadamardSix.character_mul line 29
  6. lemma OAI.HadamardSix.character_perm line 33
  7. lemma OAI.HadamardSix.character_norm line 37
  8. lemma OAI.HadamardSix.character_neg line 41
  9. lemma OAI.HadamardSix.character_constant line 49
  10. lemma OAI.HadamardSix.g_zero line 61
  11. lemma OAI.HadamardSix.g_neg line 64
  12. lemma OAI.HadamardSix.g_norm_le_one line 70
  13. lemma OAI.HadamardSix.g_permuteCharge line 78
  14. lemma OAI.HadamardSix.g_permute_columns line 86
  15. lemma OAI.HadamardSix.g_row_phases line 91
  16. lemma OAI.HadamardSix.g_column_phases line 96
  17. def OAI.HadamardSix.differenceCharge line 101
  18. lemma OAI.HadamardSix.differenceCharge_balanced line 104
  19. lemma OAI.HadamardSix.character_single line 108
  20. lemma OAI.HadamardSix.character_difference line 118
  21. lemma OAI.HadamardSix.g_difference line 125
  22. def OAI.HadamardSix.entrywiseSquare line 130

    Also declared: ComparatorChallenges/HadamardCubeFiber.lean:19 (same declaration text).

  23. lemma OAI.HadamardSix.Unimodular.entrywiseSquare line 132
  24. lemma OAI.HadamardSix.six_mul_g_double_difference line 137
  25. lemma OAI.HadamardSix.square_hadamard_iff line 142