OAI/Analysis/MutuallyUnbiased/Completion/OrthogonalPinching.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MUB6.Weiner.SuperSix line 13
2. lemma OAI.MUB6.Weiner.six_projection_sum_square line 15
3. lemma OAI.MUB6.Weiner.seven_projection_sum_square line 26
4. lemma OAI.MUB6.Weiner.projection_sum_mul_traceMatrix line 37
5. lemma OAI.MUB6.Weiner.traceMatrix_mul_projection_sum line 43
6. lemma OAI.MUB6.Weiner.traceMatrix_six_square line 49
7. theorem OAI.MUB6.Weiner.six_complement_idempotent line 58

   Source documentation

   Six mutually unbiased unital pinching maps give an idempotent complement.

   theorem six_complement_idempotent (D : Fin 6 → SuperSix)
       (hpair : ∀ r s, D r * D s = if r = s then D r else (1 / 6 : ℂ) • traceMatrix)
       (hherm : ∀ r, (D r)ᴴ = D r) (hunital : ∀ r, applySuper (D r) 1 = 1) :
       (1 + traceMatrix - ∑ r, D r) * (1 + traceMatrix - ∑ r, D r) =
         1 + traceMatrix - ∑ r, D r :=
   …

   Mentions: OAI.MUB6.Weiner.SuperSix, OAI.MUB6.Weiner.traceMatrix, OAI.MUB6.Weiner.applySuper

8. theorem OAI.MUB6.Weiner.seven_complement_idempotent line 68

   Source documentation

   The complete seven-basis complement is idempotent as well.

   theorem seven_complement_idempotent (D : Fin 7 → SuperSix)
       (hpair : ∀ r s, D r * D s = if r = s then D r else (1 / 6 : ℂ) • traceMatrix)
       (hherm : ∀ r, (D r)ᴴ = D r) (hunital : ∀ r, applySuper (D r) 1 = 1) :
       (1 + traceMatrix - ∑ r, D r) * (1 + traceMatrix - ∑ r, D r) =
         1 + traceMatrix - ∑ r, D r :=
   …

   Mentions: OAI.MUB6.Weiner.SuperSix, OAI.MUB6.Weiner.traceMatrix, OAI.MUB6.Weiner.applySuper