OAI/Analysis/MutuallyUnbiased/Fourier/FourierTheorem.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.pair_cross_certificate line 11
2. theorem OAI.MUB6.pair_same_certificate line 17
3. theorem OAI.MUB6.exact_dichotomy line 24

   Source documentation

   The exact pair certificates imply the manuscript's complete dichotomy.

   theorem exact_dichotomy {H : CMatrix} (hH : IsHadamard H) :
       FourierZero H ∨ IsHadamard (fun i j => H i j ^ 2) :=
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.FourierZero

4. theorem OAI.MUB6.fourier_vanishing line 30

   Source documentation

   Endpoint 1: arbitrary complex entries, full Hadamard equivalence, and the manuscript's normalized Fourier coefficient for every permuted alpha.

   theorem fourier_vanishing {H : CMatrix} (hH : IsHadamard H)
       (hTao : ¬Equivalent H tao) (π : Equiv.Perm Coord) :
       g H (permuteCharge π alpha) = 0 :=
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Equivalent, OAI.MUB6.tao, OAI.MUB6.Coord, OAI.MUB6.g, OAI.MUB6.permuteCharge, OAI.MUB6.alpha