OAI/Analysis/MutuallyUnbiased/Completion/Frame.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Rank-one frame identities used to calculate the complement projection.

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

    Source documentation

    Sum of the rank-one operators of a finite vector family.

    def frameOperator (v : κ → I → ℂ) : Matrix I I ℂ :=
…
  2. lemma OAI.MUB6.Weiner.frameOperator_idempotent line 18
  3. lemma OAI.MUB6.Weiner.frameOperator_mul line 26
  4. lemma OAI.MUB6.Weiner.frameOperator_mulVec line 35
  5. lemma OAI.MUB6.Weiner.frameOperator_mulVec_of_inner line 39
  6. lemma OAI.MUB6.Weiner.frameOperator_mulVec_self line 44
  7. lemma OAI.MUB6.Weiner.dotProduct_mulVec_of_hermitian line 51

    Source documentation

    Transfer a Hermitian matrix across the complex dot product.

    lemma dotProduct_mulVec_of_hermitian [DecidableEq n] (C : Matrix n n ℂ)
    (hC : Cᴴ = C) (u v : n → ℂ) :
    star u ⬝ᵥ (C *ᵥ v) = star (C *ᵥ u) ⬝ᵥ v := by
…
  8. lemma OAI.MUB6.Weiner.dotProduct_fixed_of_image line 56
  9. def OAI.MUB6.Weiner.projectorVector line 68

    Source documentation

    Flatten the rank-one matrix associated with an arbitrary complex vector.

    def projectorVector (v : n → ℂ) : n × n → ℂ := fun p => v p.1 * star (v p.2)
  10. lemma OAI.MUB6.Weiner.projectorVector_inner line 70
  11. lemma OAI.MUB6.Weiner.pinchingMatrix_eq_frameOperator line 83