OAI/LinearAlgebra/Hadamard/TaoSymmetry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cubic roots of unity and complex symmetries of Tao's matrix.

  1. lemma OAI.HadamardSix.CubicSymmetry.omega_ne_zero line 9
  2. lemma OAI.HadamardSix.CubicSymmetry.omega_norm line 12
  3. lemma OAI.HadamardSix.CubicSymmetry.omega_cube line 16
  4. lemma OAI.HadamardSix.CubicSymmetry.omega_zpow_three line 29
  5. lemma OAI.HadamardSix.CubicSymmetry.omega_zpow_mod_three line 32
  6. lemma OAI.HadamardSix.CubicSymmetry.omega_zpow_eq_of_zmod_eq line 41
  7. lemma OAI.HadamardSix.CubicSymmetry.omega_zpow_neg_star line 48
  8. lemma OAI.HadamardSix.CubicSymmetry.tao_unimodular line 53
  9. lemma OAI.HadamardSix.CubicSymmetry.zmod_three_nonzero_sign line 57
  10. theorem OAI.HadamardSix.CubicSymmetry.every_row_permutation_complex line 62

    Source documentation

    Every specified row permutation extends on the literal cubic matrix.

    theorem every_row_permutation_complex (p : Equiv.Perm Index) :
    ∃ (q : Equiv.Perm Index) (conjugate : Bool)
      (U V : Index → ℂ),
      (∀ i, ‖U i‖ = 1) ∧
      (∀ j, ‖V j‖ = 1) ∧
      ∀ i j,
        taoMatrix (p i) (q j) =
          U i * V j *
            (if conjugate then star (taoMatrix i j)
             else taoMatrix i j) := by
…

    Mentions: OAI.HadamardSix.Index, OAI.HadamardSix.taoMatrix