OAI/Analysis/MutuallyUnbiased/MixedMoments/MixedMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.mixedIntegrand line 10
2. def OAI.MUB6.mixedMoment line 16

   Source documentation

   The real mixed moment with uniform reference, row injection, and injection of the distinct matrix labels into the six nonreference bases.

   def mixedMoment {p n l : ℕ} (B : Fin 7 → Basis) (A : Matrix (Fin p) (Fin n) ℤ)
       (label : Fin n → Fin l) : ℝ :=
   …

   Mentions: OAI.MUB6.Basis

3. theorem OAI.MUB6.mixedMoment_abs_le_one line 21
4. theorem OAI.MUB6.mixedMoment_empty line 35
5. theorem OAI.MUB6.mixedMoment_neg line 39
6. theorem OAI.MUB6.mixedMoment_factor_permutation line 56
7. theorem OAI.MUB6.rowFourier_row_permutation line 68
8. theorem OAI.MUB6.mixedMoment_row_permutation line 81
9. theorem OAI.MUB6.mixedMoment_label_permutation line 97
10. theorem OAI.MUB6.mixedMoment_order_one line 111