OAI/Analysis/MutuallyUnbiased/Cubic/CubicPositivity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.triple_difference line 11
2. theorem OAI.MUB6.character_triple_difference line 17
3. theorem OAI.MUB6.triple_difference_sum line 24
4. theorem OAI.MUB6.cubic_fourier_nonnegative line 40

   Source documentation

   The cubic off-diagonal Fourier sum is bounded below by minus the dimension. It is the average of squared absolute values of column power sums, minus six.

   theorem cubic_fourier_nonnegative {H : CMatrix} (hH : IsHadamard H) :
       0 ≤ 6 + offDiagSum (fun i j => (g H ((3 : ℤ) • difference i j)).re) := by
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.offDiagSum, OAI.MUB6.g, OAI.MUB6.difference