OAI/Analysis/MutuallyUnbiased/Bases/CompleteFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.relativeMatrix line 13

   Source documentation

   The six transitions from a fixed reference basis, with that basis omitted.

   def relativeMatrix (B : Fin 7 → Basis) (r : Fin 7) (s : Coord) : CMatrix :=
   …

   Mentions: OAI.MUB6.Basis, OAI.MUB6.Coord, OAI.MUB6.CMatrix

2. theorem OAI.MUB6.relativeMatrix_isHadamard line 16
3. theorem OAI.MUB6.relativeMatrix_cross line 20
4. def OAI.MUB6.fourthProduct line 29
5. theorem OAI.MUB6.relativeMatrix_order_two_expansion line 33
6. theorem OAI.MUB6.fourthProduct_self_zero line 57
7. theorem OAI.MUB6.complete_family_order_two line 67

   Source documentation

   The order-two Fourier sum identity of a complete mutually unbiased family.

   theorem complete_family_order_two (B : Fin 7 → Basis) (hB : IsMUBFamily B)
       (r : Fin 7) {a : Charge} (ha : Balanced a) (ho : order a = 2) :
       ∑ s, g (relativeMatrix B r s) a = 0 := by
   …

   Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Charge, OAI.MUB6.Balanced, OAI.MUB6.order, OAI.MUB6.g, OAI.MUB6.relativeMatrix