OAI/Analysis/MutuallyUnbiased/Completion/BasisFrame.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The rank-one frames associated with actual orthonormal and unbiased bases.

  1. def OAI.MUB6.Weiner.basisCoordinates line 15

    Source documentation

    Ordinary complex coordinates of an orthonormal basis.

    noncomputable def basisCoordinates (b : MUB6.Basis) : Coord → Coord → ℂ := fun a i => b a i

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

  2. def OAI.MUB6.Weiner.traceVector line 17
  3. lemma OAI.MUB6.Weiner.basisCoordinates_unit line 19
  4. lemma OAI.MUB6.Weiner.basisCoordinates_complete line 24
  5. lemma OAI.MUB6.Weiner.basis_projectorVector_sum line 32
  6. lemma OAI.MUB6.Weiner.traceVector_outer line 38
  7. lemma OAI.MUB6.Weiner.basis_projector_inner line 44
  8. lemma OAI.MUB6.Weiner.basis_pinching_idempotent line 55
  9. lemma OAI.MUB6.Weiner.mub_pinching_mul line 65
  10. lemma OAI.MUB6.Weiner.basis_pinching_unital line 81
  11. lemma OAI.MUB6.Weiner.basis_pinching_trace line 85
  12. lemma OAI.MUB6.Weiner.basis_complement_unital line 89
  13. lemma OAI.MUB6.Weiner.basis_pinching_pair line 94
  14. lemma OAI.MUB6.Weiner.basis_complement_idempotent line 104
  15. theorem OAI.MUB6.Weiner.complete_basis_complement_eq_zero line 113

    Source documentation

    The Hilbert--Schmidt complement vanishes for seven unbiased bases.

    theorem complete_basis_complement_eq_zero (B : Fin 7 → MUB6.Basis) (hB : IsMUBFamily B) :
    complementMatrix (fun r => basisCoordinates (B r)) = 0 := by
…

    Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Weiner.complementMatrix, OAI.MUB6.Weiner.basisCoordinates

  16. theorem OAI.MUB6.Weiner.complete_basis_fourth_moment line 124

    Source documentation

    Entrywise fourth moment of a complete family of seven orthonormal bases.

    theorem complete_basis_fourth_moment (B : Fin 7 → MUB6.Basis) (hB : IsMUBFamily B)
    (i j k l : Coord) :
    (∑ r, ∑ a, B r a i * star (B r a j) * star (B r a k) * B r a l) =
      (if i = k ∧ j = l then 1 else 0) + (if i = j ∧ k = l then 1 else 0) := by
…

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

  17. lemma OAI.MUB6.Weiner.isMUBFamily_map line 136

    Source documentation

    A common unitary change of coordinates preserves mutual unbiasedness.

    lemma isMUBFamily_map {m : ℕ} (B : Fin m → MUB6.Basis) (hB : IsMUBFamily B)
    (U : Space ≃ₗᵢ[ℂ] Space) : IsMUBFamily (fun r => (B r).map U) := by
…

    Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Space

  18. theorem OAI.MUB6.Weiner.complete_basis_fourth_moment_relative line 142

    Source documentation

    The complete-family fourth moment in coordinates of any reference basis.

    theorem complete_basis_fourth_moment_relative (B : Fin 7 → MUB6.Basis) (hB : IsMUBFamily B)
    (ref : MUB6.Basis) (i j k l : Coord) :
    (∑ r, ∑ a, inner ℂ (ref i) (B r a) * star (inner ℂ (ref j) (B r a)) *
      star (inner ℂ (ref k) (B r a)) * inner ℂ (ref l) (B r a)) =
      (if i = k ∧ j = l then 1 else 0) + (if i = j ∧ k = l then 1 else 0) := by
…

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

  19. lemma OAI.MUB6.Weiner.basis_projectorVector_orthonormal line 151
  20. lemma OAI.MUB6.Weiner.basis_pinching_projectorVector line 157
  21. lemma OAI.MUB6.Weiner.mub_pinching_projectorVector line 163
  22. lemma OAI.MUB6.Weiner.traceVector_dot_projectorVector line 175
  23. lemma OAI.MUB6.Weiner.traceMatrix_projectorVector line 180
  24. lemma OAI.MUB6.Weiner.basis_complement_projectorVector line 185