TaoFourier.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fourier norm invariance for the cubic matrix under permutations and negation.

lemma OAI.HadamardSix.CubicSymmetry.character_star line 10
lemma OAI.HadamardSix.CubicSymmetry.g_star line 18
lemma OAI.HadamardSix.CubicSymmetry.norm_g_phases_columns line 23
theorem OAI.HadamardSix.CubicSymmetry.norm_g_permute line 44
Source documentation
The Fourier norm of the cubic matrix is invariant under all permutations of a balanced charge.
```
theorem norm_g_permute (a : Charge) (ha : Balanced a)
    (p : Equiv.Perm Index) :
    ‖g taoMatrix (permuteCharge p a)‖ = ‖g taoMatrix a‖ := by
…
```
Mentions: OAI.HadamardSix.Charge, OAI.HadamardSix.Balanced, OAI.HadamardSix.Index, OAI.HadamardSix.g, OAI.HadamardSix.taoMatrix, OAI.HadamardSix.permuteCharge
theorem OAI.HadamardSix.CubicSymmetry.norm_g_neg line 77
Source documentation
Negation preserves the Fourier norm even without a balance assumption.
```
theorem norm_g_neg (a : Charge) :
    ‖g taoMatrix (-a)‖ = ‖g taoMatrix a‖ := by
…
```
Mentions: OAI.HadamardSix.Charge, OAI.HadamardSix.g, OAI.HadamardSix.taoMatrix
theorem OAI.HadamardSix.CubicSymmetry.norm_g_signed_permute line 83
Source documentation
Signed permutations preserve the Fourier norm of every balanced charge.
```
theorem norm_g_signed_permute (a : Charge) (ha : Balanced a)
    (p : Equiv.Perm Index) (negate : Bool) :
    ‖g taoMatrix
        (if negate then -(permuteCharge p a) else permuteCharge p a)‖ =
      ‖g taoMatrix a‖ := by
…
```
Mentions: OAI.HadamardSix.Charge, OAI.HadamardSix.Balanced, OAI.HadamardSix.Index, OAI.HadamardSix.g, OAI.HadamardSix.taoMatrix, OAI.HadamardSix.permuteCharge
def OAI.HadamardSix.CubicSymmetry.FullCubicSymmetry line 96
Source documentation
Every row permutation of the cubic matrix extends using column permutations, unit phases and optional conjugation, and its Fourier norm is invariant under signed permutations of balanced charges.
```
def FullCubicSymmetry : Prop :=
…
```
theorem OAI.HadamardSix.CubicSymmetry.cubic_symmetry line 106