Complement.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The concrete complement supermatrix

The Hermitian and realignment symmetries are algebraic identities for arbitrary complex vectors. Orthonormality and mutual unbiasedness are needed for the separate unitality and idempotence identities.

def OAI.MUB6.Weiner.traceMatrix line 21
Source documentation
Supermatrix of the unnormalized trace map X ↦ trace(X) I.
```
def traceMatrix : Matrix (n × n) (n × n) ℂ :=
…
```
def OAI.MUB6.Weiner.pinchingMatrix line 25
Source documentation
Supermatrix of the sum of rank-one pinching maps for a vector family.
```
def pinchingMatrix (v : κ → n → ℂ) : Matrix (n × n) (n × n) ℂ :=
…
```
def OAI.MUB6.Weiner.complementMatrix line 29
Source documentation
Candidate missing-basis projection for six bases in dimension six.
```
def complementMatrix (v : ι → κ → n → ℂ) : Matrix (n × n) (n × n) ℂ :=
…
```
lemma OAI.MUB6.Weiner.traceMatrix_hermitian line 33
lemma OAI.MUB6.Weiner.pinchingMatrix_hermitian line 38
lemma OAI.MUB6.Weiner.complementMatrix_hermitian line 46
lemma OAI.MUB6.Weiner.pinchingMatrix_realigned line 52
lemma OAI.MUB6.Weiner.one_trace_realignment line 61
Source documentation
The identity and trace supermatrices interchange under realignment.
```
lemma one_trace_realignment (i j k l : n) :
    (1 : Matrix (n × n) (n × n) ℂ) (i, j) (k, l) = traceMatrix (l, j) (k, i) := by
…
```
Mentions: OAI.MUB6.Weiner.traceMatrix
lemma OAI.MUB6.Weiner.complementMatrix_realigned line 66
lemma OAI.MUB6.Weiner.applySuper_traceMatrix line 79
lemma OAI.MUB6.Weiner.traceMatrix_trace line 87
lemma OAI.MUB6.Weiner.traceMatrix_square line 92
lemma OAI.MUB6.Weiner.mul_traceMatrix_of_unital line 99
Source documentation
Composing a unital map with the trace map leaves the trace map unchanged.
```
lemma mul_traceMatrix_of_unital (C : Matrix (n × n) (n × n) ℂ)
    (hC : applySuper C 1 = 1) : C * traceMatrix = traceMatrix := by
…
```
Mentions: OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.traceMatrix
lemma OAI.MUB6.Weiner.traceMatrix_mul_of_hermitian_unital line 110
Source documentation
Self-adjoint unital maps also leave the trace map unchanged on the other side.
```
lemma traceMatrix_mul_of_hermitian_unital (C : Matrix (n × n) (n × n) ℂ)
    (hherm : Cᴴ = C) (hC : applySuper C 1 = 1) : traceMatrix * C = traceMatrix := by
…
```
Mentions: OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.traceMatrix

lemma OAI.MUB6.Weiner.pinchingMatrix_unital line 116

Source documentation

A pinching supermatrix is unital when its vectors are unit and complete.

lemma pinchingMatrix_unital (v : κ → n → ℂ)
    (hnorm : ∀ a, ∑ i, star (v a i) * v a i = 1)
    (hcomplete : ∀ i j, ∑ a, v a i * star (v a j) = if i = j then 1 else 0) :
    applySuper (pinchingMatrix v) 1 = 1 := by
…

Mentions: OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.pinchingMatrix

lemma OAI.MUB6.Weiner.pinchingMatrix_trace line 134
Source documentation
Unit input vectors give the exact trace of a pinching supermatrix.
```
lemma pinchingMatrix_trace (v : κ → n → ℂ)
    (hnorm : ∀ a, ∑ i, star (v a i) * v a i = 1) :
    (pinchingMatrix v).trace = Fintype.card κ := by
…
```
Mentions: OAI.MUB6.Weiner.pinchingMatrix

lemma OAI.MUB6.Weiner.complementMatrix_unital line 154

Source documentation

Six pinching maps in dimension six leave the identity fixed.

lemma complementMatrix_unital (v : Fin 6 → κ → Fin 6 → ℂ)
    (hnorm : ∀ r a, ∑ i, star (v r a i) * v r a i = 1)
    (hcomplete : ∀ r i j, ∑ a, v r a i * star (v r a j) = if i = j then 1 else 0) :
    applySuper (complementMatrix v) 1 = 1 := by
…

Mentions: OAI.MUB6.Weiner.applySuper, OAI.MUB6.Weiner.complementMatrix