Kraus.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite trace-preserving Kraus maps

The proof establishes the fixed-point commutation step needed in Weiner's completion argument. It replaces the appeal to two-positivity and the multiplicative domain with the squared Hilbert--Schmidt norm of each commutator.

def OAI.MUB6.Weiner.kraus line 23
Source documentation
A finite Kraus sum, with the adjoint on the left.
```
def kraus (A : ι → Matrix n n ℂ) (X : Matrix n n ℂ) : Matrix n n ℂ :=
…
```
lemma OAI.MUB6.Weiner.kraus_conjTranspose line 27
lemma OAI.MUB6.Weiner.trace_kraus line 32
theorem OAI.MUB6.Weiner.right_unital_of_trace_preserving line 40
Source documentation
A trace-preserving Kraus sum satisfies the second normalization identity.
```
theorem right_unital_of_trace_preserving (A : ι → Matrix n n ℂ)
    (htrace : ∀ X : Matrix n n ℂ, (kraus A X).trace = X.trace) :
    ∑ i, A i * (A i)ᴴ = 1 := by
…
```
Mentions: OAI.MUB6.Weiner.kraus

lemma OAI.MUB6.Weiner.commutator_trace_identity line 49

Source documentation

The trace of the sum of commutator squares.

lemma commutator_trace_identity (A : ι → Matrix n n ℂ) (X : Matrix n n ℂ) :
    ∑ i, (((X * A i - A i * X)ᴴ * (X * A i - A i * X)).trace) =
      (Xᴴ * X * (∑ i, A i * (A i)ᴴ)).trace
      + (Xᴴ * (∑ i, (A i)ᴴ * A i) * X).trace
      - (kraus A Xᴴ * X).trace - (Xᴴ * kraus A X).trace := by
…

Mentions: OAI.MUB6.Weiner.kraus

theorem OAI.MUB6.Weiner.commute_of_kraus_fixed line 68
Source documentation
Fixed points of a unital trace-preserving finite Kraus sum commute with its Kraus operators. The result needs no positivity axioms or external solver.
```
theorem commute_of_kraus_fixed (A : ι → Matrix n n ℂ)
    (hleft : ∑ i, (A i)ᴴ * A i = 1)
    (hright : ∑ i, A i * (A i)ᴴ = 1)
    (X : Matrix n n ℂ) (hX : kraus A X = X) (i : ι) :
    Commute X (A i) := by
…
```
Mentions: OAI.MUB6.Weiner.kraus