ProjectionBasis.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Rank-one projectors fixed by a realigned orthogonal projection

The fixed space of the complement operator contains the projectors of an orthonormal basis. This is the spectral part of the completion argument.

def OAI.MUB6.Weiner.projector line 23
Source documentation
The matrix of the orthogonal rank-one operator associated with a vector.
```
def projector (v : EuclideanSpace ℂ n) : Matrix n n ℂ :=
…
```
lemma OAI.MUB6.Weiner.toEuclideanLin_projector line 26

def OAI.MUB6.Weiner.hermitianColumn line 32

Source documentation

The real and imaginary parts of the reshaped columns.

noncomputable def hermitianColumn (C : Matrix (n × n) (n × n) ℂ)
    (p : Bool × (n × n)) : Matrix n n ℂ :=
…

lemma OAI.MUB6.Weiner.hermitianColumn_isHermitian line 38
lemma OAI.MUB6.Weiner.hermitianColumn_fixed line 46

theorem OAI.MUB6.Weiner.exists_fixed_projection_basis line 61

Source documentation

Every unital, Hermitian, idempotent, realigned superoperator fixes all the rank-one coordinate projectors of some orthonormal basis.

theorem exists_fixed_projection_basis (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hidem : C * C = C) (hreal : IsRealigned C)
    (hunital : applySuper C 1 = 1) :
    ∃ b : OrthonormalBasis (Fin (Fintype.card n)) ℂ (EuclideanSpace ℂ n),
      ∀ j, applySuper C (projector (b j)) = projector (b j) := by
…

Mentions: OAI.MUB6.Weiner.IsRealigned, OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.projector