OAI/Analysis/MutuallyUnbiased/Fourier/Dichotomy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.FourierZero line 10
2. def OAI.MUB6.PairProductsZero line 13
3. theorem OAI.MUB6.doubleDifference_zero_of_pair_products line 18
4. theorem OAI.MUB6.pair_products_row_permutation line 35
5. theorem OAI.MUB6.dichotomy_of_pair_products line 42

   Source documentation

   The manuscript's single-matrix dichotomy, conditional here only on the two explicit pair-product identities. The finite certificate supplies them.

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

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

6. theorem OAI.MUB6.dichotomy_of_pair_certificates line 58