Superoperator.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Realignment of a self-adjoint projection

The complement operator in Weiner's argument is an orthogonal projection whose matrix is invariant under realignment. Its columns therefore form a finite Kraus family; choosing an orthonormal basis of its range is unnecessary.

def OAI.MUB6.Weiner.applySuper line 21
Source documentation
Apply a matrix on pairs of indices to an ordinary matrix.
```
def applySuper (C : Matrix (n × n) (n × n) ℂ) (X : Matrix n n ℂ) : Matrix n n ℂ :=
…
```
lemma OAI.MUB6.Weiner.applySuper_add line 25
lemma OAI.MUB6.Weiner.applySuper_sub line 31
lemma OAI.MUB6.Weiner.applySuper_smul line 37
lemma OAI.MUB6.Weiner.applySuper_real_smul line 43
lemma OAI.MUB6.Weiner.applySuper_one line 47
lemma OAI.MUB6.Weiner.applySuper_add_left line 52
lemma OAI.MUB6.Weiner.applySuper_sub_left line 58
lemma OAI.MUB6.Weiner.applySuper_sum_left line 64
def OAI.MUB6.Weiner.superColumn line 72
Source documentation
A column of a superoperator, reshaped as an ordinary matrix.
```
def superColumn (C : Matrix (n × n) (n × n) ℂ) (p : n × n) : Matrix n n ℂ :=
…
```
def OAI.MUB6.Weiner.IsRealigned line 76
Source documentation
The realignment symmetry relevant to a Kraus decomposition.
```
def IsRealigned (C : Matrix (n × n) (n × n) ℂ) : Prop :=
…
```
lemma OAI.MUB6.Weiner.superColumn_fixed line 80
lemma OAI.MUB6.Weiner.applySuper_one_entry line 85

theorem OAI.MUB6.Weiner.applySuper_trace line 90

Source documentation

A self-adjoint unital superoperator preserves the ordinary matrix trace.

theorem applySuper_trace (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hunital : applySuper C 1 = 1) (X : Matrix n n ℂ) :
    (applySuper C X).trace = X.trace := by
…

Mentions: OAI.MUB6.Weiner.applySuper

theorem OAI.MUB6.Weiner.applySuper_eq_kraus_columns line 112
Source documentation
A Hermitian idempotent invariant under realignment is a Kraus sum of its reshaped columns.
```
theorem applySuper_eq_kraus_columns (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hidem : C * C = C) (hreal : IsRealigned C)
    (X : Matrix n n ℂ) : applySuper C X = kraus (superColumn C) X := by
…
```
Mentions: OAI.MUB6.Weiner.IsRealigned, OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.kraus, OAI.MUB6.Weiner.superColumn
lemma OAI.MUB6.Weiner.applySuper_conjTranspose line 144
lemma OAI.MUB6.Weiner.applySuper_eq_sum_smul_columns line 150
theorem OAI.MUB6.Weiner.commute_of_super_fixed line 158
Source documentation
Every fixed point of a unital realigned orthogonal projection commutes with every reshaped column of that projection.
```
theorem commute_of_super_fixed (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hidem : C * C = C) (hreal : IsRealigned C)
    (hunital : applySuper C 1 = 1)
    (X : Matrix n n ℂ) (hX : applySuper C X = X) (p : n × n) :
    Commute X (superColumn C p) := by
…
```
Mentions: OAI.MUB6.Weiner.IsRealigned, OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.superColumn
theorem OAI.MUB6.Weiner.super_fixedPoints_commute line 176
Source documentation
The entire fixed space is commutative. Its elements are linear combinations of the reshaped columns, which all commute with every fixed point.
```
theorem super_fixedPoints_commute (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hidem : C * C = C) (hreal : IsRealigned C)
    (hunital : applySuper C 1 = 1) (X Y : Matrix n n ℂ)
    (hX : applySuper C X = X) (hY : applySuper C Y = Y) : Commute X Y := by
…
```
Mentions: OAI.MUB6.Weiner.IsRealigned, OAI.MUB6.Weiner.applySuper

theorem OAI.MUB6.Weiner.superColumns_commute line 186

Source documentation

In particular the reshaped columns all commute.

theorem superColumns_commute (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hidem : C * C = C) (hreal : IsRealigned C)
    (hunital : applySuper C 1 = 1) (p q : n × n) :
    Commute (superColumn C p) (superColumn C q) :=
…

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

theorem OAI.MUB6.Weiner.hermitian_idempotent_eq_zero_of_trace_zero line 194

Source documentation

A Hermitian idempotent with zero trace is zero.

theorem hermitian_idempotent_eq_zero_of_trace_zero {I : Type*} [Fintype I]
    (C : Matrix I I ℂ) (hherm : Cᴴ = C) (hidem : C * C = C)
    (htrace : C.trace = 0) : C = 0 := by
…