DifferentMatrices.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.difference_reverse line 11
theorem OAI.MUB6.cross_character_gram line 14
theorem OAI.MUB6.cross_character_offdiag line 27
theorem OAI.MUB6.weighted_cross_character line 39
theorem OAI.MUB6.g_product_expand line 54
theorem OAI.MUB6.different_matrices_identity line 67
Source documentation
The different-matrix Fourier identity from unbiasedness of every pair of columns. The off-diagonal indexing lists each difference e_i-e_j once.
```
theorem different_matrices_identity {H K : CMatrix} (hH : IsHadamard H) (hK : IsHadamard K)
    (hc : ∀ k l, Complex.normSq (∑ i, H i k * conj (K i l)) = 6) (a b : Charge) :
    offDiagSum (fun i j => g H (a + difference i j) * g K (b + difference j i)) = 0 := by
…
```
Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Charge, OAI.MUB6.offDiagSum, OAI.MUB6.g, OAI.MUB6.difference