1. PhyslibAlpha
  2. QuantumMechanics
  3. StinespringDilation
Imports
/- Copyright (c) 2026 Bjørn Kjos-Hanssen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bjørn Kjos-Hanssen -/ module public import Mathlib.Data.Matrix.PEquiv public import Mathlib.Probability.Distributions.Poisson.Basic public import Mathlib.Analysis.Normed.Lp.lpSpace public import Physlib.Meta.TODO.Basic public import Mathlib

Stinespring dilation

@[expose] public sectionTODO "There is a different version of the Stienspring dilation in `QuantumInfo.Channels.CPTP`. We should unify the the version here with that one. Some of the definitions here are more general then the ones in `QuantumInfo` as they do not restrict to `ℂ`. This is something we should modify in `QuantumInfo`."

Completely positive map given by a (not necessarily minimal) Kraus family.

def krausApply {R : Type*} [Mul R] [Star R] [AddCommMonoid R] {q r : Type*} [Fintype q] [Fintype r] (K : r → Matrix q q R) (ρ : Matrix q q R) : Matrix q q R := ∑ i, K i * ρ * (K i)ᴴ

Kraus operator preserves PSD property.

lemma krausApply.posSemidef {R : Type*} [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {q r : Type*} [Fintype q] [Fintype r] (K : r → Matrix q q R) {ρ : Matrix q q R} (hρ : ρ.PosSemidef) : (krausApply K ρ).PosSemidef := posSemidef_sum _ fun _ _ => hρ.mul_mul_conjTranspose_same _

Quantum channel.

def QuantumChannel {R : Type*} [Mul R] [One R] [Star R] [AddCommMonoid R] {q r : Type*} [Fintype q] [Fintype r] [DecidableEq q] (K : r → Matrix q q R) := ∑ i, (K i)ᴴ * K i = 1

Quantum operation.

def QuantumOperation {R : Type*} [RCLike R] {q r : Type*} [Fintype q] [Fintype r] [DecidableEq q] (K : r → Matrix q q R) := ∑ i, (K i)ᴴ * K i ≤ 1

Density matrix.

def densityMatrix {R : Type*} [Ring R] [PartialOrder R] [StarRing R] (d : Type*) [Fintype d] := {ρ : Matrix d d R // ρ.PosSemidef ∧ ρ.trace = 1}

Density matrices are closed under real convex combinations.

R:Type u_1inst✝:RCLike Rd:ℕρ₀:densityMatrix (Fin d)ρ₁:densityMatrix (Fin d)t:Rhp₀:0 ≤ thp₁:0 ≤ 1 - t⊢ t * 1 + (1 - t) • 1 = 1 All goals completed! 🐙⟩

Also known as partialTraceRight.

def tr₂ {R : Type*} [Ring R] {m n m' : Type*} [Fintype n] (ρ : Matrix (m × n) (m' × n) R) : Matrix m m' R := fun i j => ∑ k, ρ (i, k) (j, k)

stinespringOp is often written as V.

def stinespringOp {R : Type*} [Ring R] {m r : Type*} [Fintype r] [DecidableEq r] (K : r → Matrix m m R) : Matrix (m × r) m R := let V₀ : Matrix (m × r) (m × Fin 1) R := ∑ i, K i ⊗ₖ single i (0 : Fin 1) (1 : R) fun x y => V₀ x (y,0)

The Stinespring dilation.

def stinespringDilation {R : Type*} [Ring R] [StarRing R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] (K : r → Matrix m m R) (ρ : Matrix m m R) := let V := stinespringOp K; V * ρ * Vᴴ

The partial trace of the Stinespring dilation.

def stinespringForm {R : Type*} [Ring R] [StarRing R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] (K : r → Matrix m m R) := fun ρ => tr₂ (stinespringDilation K ρ)

A useful identity for Stinespring dilations.

R:Type u_1inst✝⁴:Ring Rinst✝³:StarRing Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Ri:mj:m⊢ ∑ c, (star K c * K c) i j = ∑ j_1, (have V₀ := ∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1); fun x y => V₀ x (y, 0))ᴴ i j_1 * (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) j_1 (j, 0) R:Type u_1inst✝⁴:Ring Rinst✝³:StarRing Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Ri:mj:m⊢ ∑ x, ∑ x_1, star (K x x_1 i) * K x x_1 j = ∑ x, star (K x.2 x.1 i) * K x.2 x.1 j; erw [ R:Type u_1inst✝⁴:Ring Rinst✝³:StarRing Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Ri:mj:m⊢ ∑ x, ∑ x_1, star (K x x_1 i) * K x x_1 j = ∑ x, ∑ y, star (K (x, y).2 (x, y).1 i) * K (x, y).2 (x, y).1 j R:Type u_1inst✝⁴:Ring Rinst✝³:StarRing Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Ri:mj:m⊢ ∑ y, ∑ x, star (K x y i) * K x y j = ∑ x, ∑ y, star (K (x, y).2 (x, y).1 i) * K (x, y).2 (x, y).1 j All goals completed! 🐙

A useful identity for completely positive, trace non-increasing maps.

R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mK:r → Matrix m m RhK:∑ i, (K i)ᴴ * K i ≤ 1⊢ ∑ i, star K i * K i = ∑ i, (K i)ᴴ * K i All goals completed! 🐙

The Stinespring operator of a completely positive, trace-preserving maps is an isometry. (Note that stinespringOp K is not a square matrix in general.)

R:Type u_1inst✝⁵:Ring Rinst✝⁴:StarRing Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mK:r → Matrix m m RhK:∑ i, (K i)ᴴ * K i = 1⊢ ∑ i, star K i * K i = ∑ i, (K i)ᴴ * K i All goals completed! 🐙

Proving the columns of V = stinespringOp K are independent is a step on the way to constructing the unitary dilation.

R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mK:r → Matrix m m RhK:∑ i, (K i)ᴴ * K i = 1i:mj:mh₁:∑ j_1, (stinespringOp K)ᴴ i j_1 * stinespringOp K j_1 j = 0g₀:¬i = jthis:1 i j = 0⊢ inner R (WithLp.toLp 2 fun i_1 => stinespringOp K i_1 i) (WithLp.toLp 2 fun i => stinespringOp K i j) = ∑ j_1, (stinespringOp K)ᴴ i j_1 * stinespringOp K j_1 j R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mK:r → Matrix m m RhK:∑ i, (K i)ᴴ * K i = 1i:mj:mh₁:∑ j_1, (stinespringOp K)ᴴ i j_1 * stinespringOp K j_1 j = 0g₀:¬i = jthis:1 i j = 0⊢ ∑ x, stinespringOp K x j * (starRingEnd R) (stinespringOp K x i) = ∑ x, (starRingEnd R) (stinespringOp K x i) * stinespringOp K x j R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mK:r → Matrix m m RhK:∑ i, (K i)ᴴ * K i = 1i:mj:mh₁:∑ j_1, (stinespringOp K)ᴴ i j_1 * stinespringOp K j_1 j = 0g₀:¬i = jthis:1 i j = 0⊢ (fun x => stinespringOp K x j * (starRingEnd R) (stinespringOp K x i)) = fun x => (starRingEnd R) (stinespringOp K x i) * stinespringOp K x j R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mK:r → Matrix m m RhK:∑ i, (K i)ᴴ * K i = 1i:mj:mh₁:∑ j_1, (stinespringOp K)ᴴ i j_1 * stinespringOp K j_1 j = 0g₀:¬i = jthis:1 i j = 0x:m × r⊢ stinespringOp K x j * (starRingEnd R) (stinespringOp K x i) = (starRingEnd R) (stinespringOp K x i) * stinespringOp K x j All goals completed! 🐙

m will of course be finite and bounded by n here, but no need to assume or prove that.

lemma basisCard {R : Type*} [RCLike R] {n m : Type*} [Fintype n] {s : Matrix n m R} (ho : Orthonormal R fun j ↦ WithLp.toLp 2 fun i ↦ s i j) : Fintype.card n = ho.toSubtypeRange.exists_orthonormalBasis_extension.choose.card := Fintype.card_coe _ ▸ (Nat.cast_inj.mp <| (rank_eq_card_basis <| PiLp.basisFun _ _ _).symm.trans <| rank_eq_card_basis ho.toSubtypeRange.exists_orthonormalBasis_extension.choose_spec.choose.toBasis)

Calculating the cardinality of the orthonormal basis obtained by extending the Stinespring orthonormal set, the columns of stinespringOp K.

lemma stinespringCard {R : Type*} [RCLike R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] {K : r → Matrix m m R} (hK : ∑ i, (K i)ᴴ * K i = 1) : Fintype.card (m × r) = (stinespringOrtho hK).toSubtypeRange.exists_orthonormalBasis_extension.choose.card := basisCard <| stinespringOrtho hK

See discussion at https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/succAbove.20and.20predAbove.20lemmas/with/584270574

def Fin.predAbove_of_ne {n : ℕ} {k i : Fin n} (h : i ≠ k) : Fin (n - 1) := n:ℕk:Fin ni:Fin nh:i ≠ k⊢ Fin (n - 1) n:ℕk:Fin ni:Fin nh:i ≠ kH:↑i > ↑k⊢ Fin (n - 1)n:ℕk:Fin ni:Fin nh:i ≠ kH:¬↑i > ↑k⊢ Fin (n - 1) n:ℕk:Fin ni:Fin nh:i ≠ kH:↑i > ↑k⊢ Fin (n - 1) exact ⟨i.1 - 1, n:ℕk:Fin ni:Fin nh:i ≠ kH:↑i > ↑k⊢ ↑i - 1 < n - 1 All goals completed! 🐙⟩ n:ℕk:Fin ni:Fin nh:i ≠ kH:¬↑i > ↑k⊢ Fin (n - 1) exact ⟨i.1, n:ℕk:Fin ni:Fin nh:i ≠ kH:¬↑i > ↑k⊢ ↑i < n - 1 All goals completed! 🐙⟩

A "missing lemma" for Fin types.

lemma Fin.predAbove_of_ne_injective (n : ℕ) (k x y : Fin n) (hx : x ≠ k) (hy : y ≠ k) (heq : Fin.predAbove_of_ne hx = Fin.predAbove_of_ne hy) : x = y := n:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kheq:predAbove_of_ne hx = predAbove_of_ne hy⊢ x = y n:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kheq:(if H : ↑x > ↑k then ⟨↑x - 1, ⋯⟩ else ⟨↑x, ⋯⟩) = if H : ↑y > ↑k then ⟨↑y - 1, ⋯⟩ else ⟨↑y, ⋯⟩⊢ x = y n:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kh✝¹:↑x > ↑kh✝:↑y > ↑kheq:⟨↑x - 1, ⋯⟩ = ⟨↑y - 1, ⋯⟩⊢ x = yn:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kh✝¹:↑x > ↑kh✝:¬↑y > ↑kheq:⟨↑x - 1, ⋯⟩ = ⟨↑y, ⋯⟩⊢ x = yn:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kh✝¹:¬↑x > ↑kh✝:↑y > ↑kheq:⟨↑x, ⋯⟩ = ⟨↑y - 1, ⋯⟩⊢ x = yn:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kh✝¹:¬↑x > ↑kh✝:¬↑y > ↑kheq:⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩⊢ x = y all_goals n:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kh✝¹:¬↑x > ↑kh✝:¬↑y > ↑kheq:⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩⊢ x = y n:ℕk:Fin nx:Fin ny:Fin nhx:x ≠ khy:y ≠ kh✝¹:¬↑x > ↑kh✝:¬↑y > ↑kheq:↑x = ↑y⊢ x = y All goals completed! 🐙

The way this is written, Fin r and Fin (r-1) both occur so it is tricky to go to a general Fintype.

def onbPart {R : Type*} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i, (K i)ᴴ * K i = 1) (x : Fin m × Fin r) {z : Fin r} (hx : ¬x.2 = z) : -- if we make it `r+2` then the `x.2≠0` becomes unused. Fin m × Fin r → R := R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1x:Fin m × Fin rz:Fin rhx:¬x.2 = z⊢ Fin m × Fin r → R R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1x:Fin m × Fin rz:Fin rhx:¬x.2 = ztheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)⊢ Fin m × Fin r → R R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1x:Fin m × Fin rz:Fin rhx:¬x.2 = ztheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)this:Fin m × Fin (r - 1) → Fin m × Fin r → R⊢ Fin m × Fin r → R R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1x:Fin m × Fin rz:Fin rhx:¬x.2 = ztheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)this:Fin m × Fin (r - 1) → Fin m × Fin r → R⊢ Fin m × Fin (r - 1) All goals completed! 🐙
R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ry:Fin m × Fin rhy:¬y.2 = zx:Fin m × Fin rhx:¬x.2 = zh:y ≠ xtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)α:∃ b, ⇑b = Subtype.val := ···this:∀ (a : WithLp 2 (Fin m × Fin r → R)) (b : a ∈ theRangeᗮ) (b_1 : ⟨a, b⟩ ∈ ⋯.choose) (a_1 : WithLp 2 (Fin m × Fin r → R)) (b_2 : a_1 ∈ theRangeᗮ) (b_3 : ⟨a_1, b_2⟩ ∈ ⋯.choose), ¬a = a_1 → inner R ↑(α.choose ⟨⟨a, b⟩, b_1⟩) ↑(α.choose ⟨⟨a_1, b_2⟩, b_3⟩) = 0h₁:inner R ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK y hy), ⋯⟩, ⋯⟩) ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK x hx), ⋯⟩, ⋯⟩) = 0⊢ inner R (WithLp.toLp 2 (onbPart hK y hy)) (WithLp.toLp 2 (onbPart hK x hx)) = inner R ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK y hy), ⋯⟩, ⋯⟩) ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK x hx), ⋯⟩, ⋯⟩) simp_rw R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ry:Fin m × Fin rhy:¬y.2 = zx:Fin m × Fin rhx:¬x.2 = zh:y ≠ xtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)α:∃ b, ⇑b = Subtype.val := ···this:∀ (a : WithLp 2 (Fin m × Fin r → R)) (b : a ∈ theRangeᗮ) (b_1 : ⟨a, b⟩ ∈ ⋯.choose) (a_1 : WithLp 2 (Fin m × Fin r → R)) (b_2 : a_1 ∈ theRangeᗮ) (b_3 : ⟨a_1, b_2⟩ ∈ ⋯.choose), ¬a = a_1 → inner R ↑(α.choose ⟨⟨a, b⟩, b_1⟩) ↑(α.choose ⟨⟨a_1, b_2⟩, b_3⟩) = 0h₁:inner R ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK y hy), ⋯⟩, ⋯⟩) ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK x hx), ⋯⟩, ⋯⟩) = 0⊢ inner R (WithLp.toLp 2 (onbPart hK y hy)) (WithLp.toLp 2 (onbPart hK x hx)) = inner R ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK y hy), ⋯⟩, ⋯⟩) ↑(α.choose ⟨⟨WithLp.toLp 2 (onbPart hK x hx), ⋯⟩, ⋯⟩)All goals completed! 🐙]

The vectors in the Stinespring orthonormal basis have norm 1.

lemma onbPart_norm {R : Type*} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i, (K i)ᴴ * K i = 1) (x : Fin m × Fin r) {z : Fin r} (hx : ¬x.2 = z) : ‖WithLp.toLp 2 <| onbPart hK x hx‖ = 1 := let theRange := Submodule.span R <| Set.range fun j => WithLp.toLp 2 fun i ↦ stinespringOp K i j (exists_orthonormalBasis R theRangeᗮ).choose_spec.choose.orthonormal.1 _

Also known as unitaryDilation. Respects x,y order.

def Ud {R : Type*} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i, (K i)ᴴ * K i = 1) (z : Fin r) : Matrix (Fin m × Fin r) (Fin m × Fin r) R := R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin r⊢ Matrix (Fin m × Fin r) (Fin m × Fin r) R R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rx:Fin m × Fin ry:Fin m × Fin r⊢ R R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rx:Fin m × Fin ry:Fin m × Fin rhy:y.2 = z⊢ RR:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rx:Fin m × Fin ry:Fin m × Fin rhy:¬y.2 = z⊢ R R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rx:Fin m × Fin ry:Fin m × Fin rhy:y.2 = z⊢ R All goals completed! 🐙 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rx:Fin m × Fin ry:Fin m × Fin rhy:¬y.2 = z⊢ R All goals completed! 🐙

This generalization of Stinespring dilation has the right "shape" but otherwise nothing specific to it.

def general_dilation {R : Type*} {m r : Type*} [DecidableEq r] (z : r) (S : Matrix (m × r) m R) (M : Matrix (m × r) (m × r) R) : Matrix (m × r) (m × r) R := fun x y => ite (y.2 = z) (S x y.1) (M x y)

A general, not necessarily unitary, dilation.

def dilation {R : Type*} [Ring R] {m r : Type*} [Fintype r] [DecidableEq r] (K : r → Matrix m m R) (z : r) (M : Matrix (m × r) (m × r) R) : Matrix (m × r) (m × r) R := general_dilation z (stinespringOp K) (M)

One version of orthonormality of stinespringOp.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ri:Fin m × Fin rj:Fin m × Fin rh:i ≠ jtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)g₀:¬i.2 = zg₂:j.2 = zh₀':(WithLp.toLp 2 fun i_1 => stinespringOp K i_1 j.1) ∈ theRangeh₁:(WithLp.toLp 2 fun t => onbPart hK i g₀ t) ∈ theRangeᗮ⊢ inner R (WithLp.toLp 2 fun i_1 => onbPart hK i g₀ i_1) (WithLp.toLp 2 fun i => stinespringOp K i j.1) = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ri:Fin m × Fin rj:Fin m × Fin rh:i ≠ jtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)g₀:¬i.2 = zg₂:j.2 = zh₀':(WithLp.toLp 2 fun i_1 => stinespringOp K i_1 j.1) ∈ theRangeh₁:(WithLp.toLp 2 fun t => onbPart hK i g₀ t) ∈ theRangeᗮthis:inner R (WithLp.toLp 2 fun i_1 => stinespringOp K i_1 j.1) (WithLp.toLp 2 fun t => onbPart hK i g₀ t) = 0⊢ inner R (WithLp.toLp 2 fun i_1 => onbPart hK i g₀ i_1) (WithLp.toLp 2 fun i => stinespringOp K i j.1) = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ri:Fin m × Fin rj:Fin m × Fin rh:i ≠ jtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)g₀:¬i.2 = zg₂:j.2 = zh₀':(WithLp.toLp 2 fun i_1 => stinespringOp K i_1 j.1) ∈ theRangeα:WithLp 2 (Fin m × Fin r → R)h₁:α ∈ theRangeᗮthis:inner R (WithLp.toLp 2 fun i_1 => stinespringOp K i_1 j.1) α = 0⊢ inner R α (WithLp.toLp 2 fun i => stinespringOp K i j.1) = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ri:Fin m × Fin rj:Fin m × Fin rh:i ≠ jtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)g₀:¬i.2 = zg₂:j.2 = zα:WithLp 2 (Fin m × Fin r → R)h₁:α ∈ theRangeᗮβ:WithLp 2 (Fin m × Fin r → R)h₀':β ∈ theRangethis:inner R β α = 0⊢ inner R α β = 0 All goals completed! 🐙 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ri:Fin m × Fin rj:Fin m × Fin rh:i ≠ jtheRange:Submodule R (WithLp 2 (Fin m × Fin r → R)) := Submodule.span R (Set.range fun j => WithLp.toLp 2 fun i => stinespringOp K i j)g₀:¬i.2 = zg₂:¬j.2 = z⊢ inner R (WithLp.toLp 2 fun i_1 => onbPart hK i g₀ i_1) (WithLp.toLp 2 fun i => onbPart hK j g₂ i) = 0 All goals completed! 🐙

The Stinespring dilation columns form an orthonormal basis.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝this:inner R (if hy : i✝.2 = z then WithLp.toLp 2 fun i => stinespringOp K i i✝.1 else WithLp.toLp 2 fun i => onbPart hK i✝ hy i) (if hy : j✝.2 = z then WithLp.toLp 2 fun i => stinespringOp K i j✝.1 else WithLp.toLp 2 fun i => onbPart hK j✝ hy i) = 0⊢ inner R (WithLp.toLp 2 fun i => if hy : i✝.2 = z then stinespringOp K i i✝.1 else onbPart hK i✝ hy i) (WithLp.toLp 2 fun i => if hy : j✝.2 = z then stinespringOp K i j✝.1 else onbPart hK j✝ hy i) = inner R (if hy : i✝.2 = z then WithLp.toLp 2 fun i => stinespringOp K i i✝.1 else WithLp.toLp 2 fun i => onbPart hK i✝ hy i) (if hy : j✝.2 = z then WithLp.toLp 2 fun i => stinespringOp K i j✝.1 else WithLp.toLp 2 fun i => onbPart hK j✝ hy i) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:i✝.2 = zg₁:j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = 0⊢ inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:i✝.2 = zg₁:¬j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => onbPart hK j✝ g₁ i) = 0⊢ inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => onbPart hK j✝ g₁ i) = inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => onbPart hK j✝ g₁ i)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:¬i✝.2 = zh✝:j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = 0⊢ inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:¬i✝.2 = zh✝:¬j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => onbPart hK j✝ h✝ i) = 0⊢ inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => onbPart hK j✝ h✝ i) = inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => onbPart hK j✝ h✝ i) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:i✝.2 = zg₁:j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = 0⊢ inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:i✝.2 = zg₁:¬j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => onbPart hK j✝ g₁ i) = 0⊢ inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => onbPart hK j✝ g₁ i) = inner R (WithLp.toLp 2 fun i => stinespringOp K i i✝.1) (WithLp.toLp 2 fun i => onbPart hK j✝ g₁ i)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:¬i✝.2 = zh✝:j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = 0⊢ inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1) = inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => stinespringOp K i j✝.1)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rh₀:Orthonormal R fun y => if hy : y.2 = z then WithLp.toLp 2 fun i => stinespringOp K i y.1 else WithLp.toLp 2 fun i => onbPart hK y hy ii✝:Fin m × Fin rj✝:Fin m × Fin rhij:i✝ ≠ j✝g₀:¬i✝.2 = zh✝:¬j✝.2 = zthis:inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => onbPart hK j✝ h✝ i) = 0⊢ inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => onbPart hK j✝ h✝ i) = inner R (WithLp.toLp 2 fun i => onbPart hK i✝ g₀ i) (WithLp.toLp 2 fun i => onbPart hK j✝ h✝ i) All goals completed! 🐙

If β has length 1 then the dot product of β with itself is 1.

R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ ‖WithLp.toLp 2 β‖ ^ 2 = ∑ x, (re (β x) * re (β x) + im (β x) * im (β x)) simp_rw R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ ‖WithLp.toLp 2 β‖ ^ 2 = ∑ x, (re (β x) * re (β x) + im (β x) * im (β x))R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ ‖WithLp.toLp 2 β‖ ^ 2 = ∑ x, ‖β x‖ ^ 2] All goals completed! 🐙 R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ im 1 = im (∑ x, (starRingEnd R) (β x) * β x) R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ 0 = ∑ x, (re (β x) * im (β x) + -(im (β x) * re (β x))) R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ ∑ x, (re (β x) * im (β x) + -(im (β x) * re (β x))) = 0 R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ ∀ (a : t), re (β a) * im (β a) + -(im (β a) * re (β a)) = 0 R:Type u_1inst✝¹:RCLike Rt:Type u_2inst✝:Fintype tβ:t → Rhj:‖WithLp.toLp 2 β‖ = 1⊢ ∀ (a : t), True All goals completed! 🐙

A matrix whose columns are orthonormal is unitary.

R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = j⊢ ∑ x, (starRingEnd R) (α i x) * α j x = 0 R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = j⊢ ∑ x, (starRingEnd R) (α i x) * α j x = inner R ((fun i => WithLp.toLp 2 (α i)) i) ((fun i => WithLp.toLp 2 (α i)) j) R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = j⊢ ∑ x, (starRingEnd R) (α i x) * α j x = ∑ x, α j x * star (α i x) R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = j⊢ (fun x => (starRingEnd R) (α i x) * α j x) = fun x => α j x * star (α i x) R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = jl:m × r⊢ (starRingEnd R) (α i l) * α j l = α j l * star (α i l) nth_rw 1 [R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = jl:m × r⊢ α j l * (starRingEnd R) (α i l) = α j l * star (α i l)R:Type u_1inst✝⁴:RCLike Rm:Type u_2r:Type u_3inst✝³:Fintype rinst✝²:DecidableEq rinst✝¹:Fintype minst✝:DecidableEq mα:Matrix (m × r) (m × r) Rh₀:Orthonormal R fun i => WithLp.toLp 2 (α i)i:m × rj:m × rH:¬i = jl:m × r⊢ α j l * (starRingEnd R) (α i l) = α j l * star (α i l) All goals completed! 🐙

The transpose of the unitary dilation is unitary.

lemma Ud_unitaryT {R : Type*} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i, (K i)ᴴ * K i = 1) (z : Fin r) : (Ud hK z)ᵀ ∈ unitary _ := R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin r⊢ (Ud hK z)ᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rH₀:(Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1⊢ (Ud hK z)ᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rH₀:(Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1⊢ star (Ud hK z)ᵀ * (Ud hK z)ᵀ = 1R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rH₀:(Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1⊢ (Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rH₀:(Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1⊢ star (Ud hK z)ᵀ * (Ud hK z)ᵀ = 1 All goals completed! 🐙 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rH₀:(Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1⊢ (Ud hK z)ᵀ * star (Ud hK z)ᵀ = 1 All goals completed! 🐙

The unitary dilation Ud is in fact unitary.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rU:Matrix (Fin m × Fin r) (Fin m × Fin r) Rthis✝:Uᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)this:star U * U = 1⊢ U ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rU:Matrix (Fin m × Fin r) (Fin m × Fin r) Rthis✝:Uᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)this:star U * U = 1⊢ star U * U = 1R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rU:Matrix (Fin m × Fin r) (Fin m × Fin r) Rthis✝:Uᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)this:star U * U = 1⊢ U * star U = 1 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rU:Matrix (Fin m × Fin r) (Fin m × Fin r) Rthis✝:Uᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)this:star U * U = 1⊢ star U * U = 1 All goals completed! 🐙 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rU:Matrix (Fin m × Fin r) (Fin m × Fin r) Rthis✝:Uᵀ ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)this:star U * U = 1⊢ U * star U = 1 All goals completed! 🐙

Taking the partial trace of a tensor product with a matrix of trace 1 is the identity map.

R:Type u_1inst✝¹:RCLike Rm:Type u_2w:Type u_3inst✝:Fintype we:Matrix w w Rρ:Matrix m m Ri:mj:mthis:∑ x, ρ i j * e x x = ρ i j * ∑ x, e x xhtr:∑ x, e x x = 1⊢ ρ i j * 1 = ρ i j All goals completed! 🐙

The Stinespring unitary form.

def stinespringUnitaryForm {R : Type*} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i, (K i)ᴴ * K i = 1) (z : Fin r) (ρ : Matrix (Fin m) (Fin m) R) : (Matrix (Fin m) (Fin m) R) := let U := Ud hK z tr₂ (U * (ρ ⊗ₖ (single z z 1)) * Uᴴ)

The Stinespring unitary form, general version.

def stinespringUnitaryForm_e {R : Type*} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i, (K i)ᴴ * K i = 1) (z : Fin r) (e : Matrix (Fin r) (Fin r) R) (ρ : Matrix (Fin m) (Fin m) R) : (Matrix (Fin m) (Fin m) R) := let U := Ud hK z tr₂ (U * (ρ ⊗ₖ e) * Uᴴ)

Trace-free version of the Stinespring Dilation Theorem.

theorem tracefree_version {R : Type*} [RCLike R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] {K : r → Matrix m m R} (ρ : Matrix m m R) : let K' := fun i x y => star <| K i y x; let U := (stinespringOp K'); Uᴴ * (ρ ⊗ₖ (1 : Matrix r r R)) * U = stinespringForm K ρ := R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m R⊢ let K' := fun i x y => star (K i y x); let U := stinespringOp K'; Uᴴ * kroneckerMap (fun x1 x2 => x1 * x2) ρ 1 * U = stinespringForm K ρ -- Since my proof broke in 4.27 -> 4.31, here's Aristotle's proof. R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m R⊢ ((fun x y => (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_1 y => (starRingEnd R) (K x y x_1)) (single x 0 1)) x (y, 0))ᴴ * kroneckerMap (fun x1 x2 => x1 * x2) ρ 1 * fun x y => (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_1 y => (starRingEnd R) (K x y x_1)) (single x 0 1)) x (y, 0)) = tr₂ ((fun x y => (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0)) * ρ * (fun x y => (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0))ᴴ); R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m Rx:my:m⊢ ((fun x y => (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_1 y => (starRingEnd R) (K x y x_1)) (single x 0 1)) x (y, 0))ᴴ * kroneckerMap (fun x1 x2 => x1 * x2) ρ 1 * fun x y => (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_1 y => (starRingEnd R) (K x y x_1)) (single x 0 1)) x (y, 0)) x y = tr₂ ((fun x y => (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0)) * ρ * (fun x y => (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0))ᴴ) x y R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m Rx:my:m⊢ ∑ x_1, (∑ x_2, if x_2.2 = x_1.2 then (starRingEnd R) ((∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_3 y => (starRingEnd R) (K x y x_3)) (single x 0 1)) x_2 (x, 0)) * ρ x_2.1 x_1.1 else 0) * (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_2 y => (starRingEnd R) (K x y x_2)) (single x 0 1)) x_1 (y, 0) = ∑ x_1, ∑ x_2, (∑ j, (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) (x, x_1) (j, 0) * ρ j x_2) * (starRingEnd R) ((∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) (y, x_1) (x_2, 0)) R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m Rx:my:m⊢ ∑ x_1, (∑ x_2, if x_2.2 = x_1.2 then (starRingEnd R) ((∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_3 y => (starRingEnd R) (K x y x_3)) (single x 0 1)) x_2 (x, 0)) * ρ x_2.1 x_1.1 else 0) * (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (fun x_2 y => (starRingEnd R) (K x y x_2)) (single x 0 1)) x_1 (y, 0) = ∑ x_1, ∑ x_2, (∑ x_3, (∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (K x) (single x 0 1)) (x, x_1) (x_3, 0) * ρ x_3 x_2) * (starRingEnd R) ((∑ x, kroneckerMap (fun x1 x2 => x1 * x2) (K x) (single x 0 1)) (y, x_1) (x_2, 0)); R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m Rx:my:m⊢ ∑ x_1, ∑ x_2, (∑ x_3, (∑ x_4, K x_4 x x_3 * (starRingEnd R) (single x_4 0 1 x_2 0)) * ρ x_3 x_1) * ∑ x, (starRingEnd R) (K x y x_1) * single x 0 1 x_2 0 = ∑ x_1, ∑ x_2, (∑ x_3, (∑ x_4, K x_4 x x_3 * single x_4 0 1 x_1 0) * ρ x_3 x_2) * ∑ x, (starRingEnd R) (K x y x_2) * (starRingEnd R) (single x 0 1 x_1 0); R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m Rx:my:m⊢ ∑ x_1, ∑ x_2, (∑ x_3, K x_2 x x_3 * ρ x_3 x_1) * (starRingEnd R) (K x_2 y x_1) = ∑ x_1, ∑ x_2, (∑ x_3, K x_1 x x_3 * ρ x_3 x_2) * (starRingEnd R) (K x_1 y x_2); All goals completed! 🐙

A Heisberg picture / Schrödinger picture view of the Stinespring dilation.

R:Type u_1inst✝³:RCLike Rm:Type u_2r:Type u_3inst✝²:Fintype rinst✝¹:DecidableEq rinst✝:Fintype mK:r → Matrix m m Rρ:Matrix m m RK':r → m → m → R := fun i x y => star (K i y x)U:Matrix (m × r) m R := stinespringOp K'⊢ let V := stinespringOp K; let schrõdinger := tr₂ (V * ρ * Vᴴ); let heisenberg := stinespringForm K ρ; schrõdinger = heisenberg All goals completed! 🐙

A further generalization of stinespringGeneralForm.

def generalForm {R : Type*} [RCLike R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] (z : r) (S : Matrix (m × r) m R) (M : Matrix (m × r) (m × r) R) := let U := general_dilation z S M fun ρ => tr₂ (U * (ρ ⊗ₖ (single z z 1)) * Uᴴ)

General form of the Stinespring dilation.

def stinespringGeneralForm {R : Type*} [RCLike R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] (K : r → Matrix m m R) (z : r) (M : Matrix (m × r) (m × r) R) := let U := dilation K z M fun ρ => tr₂ (U * (ρ ⊗ₖ (single z z 1)) * Uᴴ)

Even more general form of the Stinespring dilation.

def stinespringGeneralForm_e {R : Type*} [RCLike R] {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] (K : r → Matrix m m R) (z : r) (e : Matrix r r R) (M : Matrix (m × r) (m × r) R) := let U := dilation K z M fun ρ => tr₂ (U * (ρ ⊗ₖ e) * Uᴴ)

When we plug in M = Ud hK into the general stinespringGeneralForm, then we do get stinespringUnitaryForm hK.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (∑ x, ∑ y, if (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * single z z 1 (x, y).2 e)) * (starRingEnd R) (if e = z then stinespringOp K (x✝, c) d else if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) = (∑ x, ∑ y, if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * single z z 1 (x, y).2 e)) * (starRingEnd R) (if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (fun x => ∑ y, if (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * single z z 1 (x, y).2 e)) = fun x => ∑ y, if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * single z z 1 (x, y).2 e)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (if e = z then stinespringOp K (x✝, c) d else if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) = if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (fun x => ∑ y, if (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * single z z 1 (x, y).2 e)) = fun x => ∑ y, if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * single z z 1 (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * single z z 1 (x, y).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin m⊢ (∑ y, if (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * single z z 1 (f, y).2 e) else if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * single z z 1 (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * single z z 1 (f, y).2 e)) = ∑ y, if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * single z z 1 (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * single z z 1 (f, y).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin m⊢ (fun y => if (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * single z z 1 (f, y).2 e) else if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * single z z 1 (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * single z z 1 (f, y).2 e)) = fun y => if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * single z z 1 (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * single z z 1 (f, y).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mg:Fin r⊢ (if (f, g).2 = z then stinespringOp K (b, c) (f, g).1 * (a (f, g).1 d * single z z 1 (f, g).2 e) else if h : (f, g).2 = z then stinespringOp K (b, c) (f, g).1 * (a (f, g).1 d * single z z 1 (f, g).2 e) else onbPart hK (f, g) h (b, c) * (a (f, g).1 d * single z z 1 (f, g).2 e)) = if h : (f, g).2 = z then stinespringOp K (b, c) (f, g).1 * (a (f, g).1 d * single z z 1 (f, g).2 e) else onbPart hK (f, g) h (b, c) * (a (f, g).1 d * single z z 1 (f, g).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mg:Fin r⊢ g = z → ∀ (h : ¬g = z), stinespringOp K (b, c) f = onbPart hK (f, g) ⋯ (b, c) ∨ a f d = 0 ∨ single z z 1 g e = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mg:Fin rhg:g = z⊢ ∀ (h : ¬g = z), stinespringOp K (b, c) f = onbPart hK (f, g) ⋯ (b, c) ∨ a f d = 0 ∨ single z z 1 g e = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin m⊢ ∀ (h : ¬z = z), stinespringOp K (b, c) f = onbPart hK (f, z) ⋯ (b, c) ∨ a f d = 0 ∨ single z z 1 z e = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mh:¬z = z⊢ stinespringOp K (b, c) f = onbPart hK (f, z) ⋯ (b, c) ∨ a f d = 0 ∨ single z z 1 z e = 0 All goals completed! 🐙 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (if e = z then stinespringOp K (x✝, c) d else if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) = if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:e = z⊢ stinespringOp K (x✝, c) d = stinespringOp K (x✝, c) dR:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:¬e = z⊢ onbPart hK (d, e) ⋯ (x✝, c) = onbPart hK (d, e) ⋯ (x✝, c) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:e = z⊢ stinespringOp K (x✝, c) d = stinespringOp K (x✝, c) dR:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:¬e = z⊢ onbPart hK (d, e) ⋯ (x✝, c) = onbPart hK (d, e) ⋯ (x✝, c) All goals completed! 🐙

The Stinespring unitary form as a general form applied to the unitary dilation.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (∑ x, ∑ y, if (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * e✝ (x, y).2 e)) * (starRingEnd R) (if e = z then stinespringOp K (x✝, c) d else if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) = (∑ x, ∑ y, if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * e✝ (x, y).2 e)) * (starRingEnd R) (if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (fun x => ∑ y, if (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * e✝ (x, y).2 e)) = fun x => ∑ y, if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * e✝ (x, y).2 e)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (if e = z then stinespringOp K (x✝, c) d else if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) = if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (fun x => ∑ y, if (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * e✝ (x, y).2 e)) = fun x => ∑ y, if h : (x, y).2 = z then stinespringOp K (b, c) (x, y).1 * (a (x, y).1 d * e✝ (x, y).2 e) else onbPart hK (x, y) h (b, c) * (a (x, y).1 d * e✝ (x, y).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin m⊢ (∑ y, if (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * e✝ (f, y).2 e) else if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * e✝ (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * e✝ (f, y).2 e)) = ∑ y, if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * e✝ (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * e✝ (f, y).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin m⊢ (fun y => if (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * e✝ (f, y).2 e) else if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * e✝ (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * e✝ (f, y).2 e)) = fun y => if h : (f, y).2 = z then stinespringOp K (b, c) (f, y).1 * (a (f, y).1 d * e✝ (f, y).2 e) else onbPart hK (f, y) h (b, c) * (a (f, y).1 d * e✝ (f, y).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mg:Fin r⊢ (if (f, g).2 = z then stinespringOp K (b, c) (f, g).1 * (a (f, g).1 d * e✝ (f, g).2 e) else if h : (f, g).2 = z then stinespringOp K (b, c) (f, g).1 * (a (f, g).1 d * e✝ (f, g).2 e) else onbPart hK (f, g) h (b, c) * (a (f, g).1 d * e✝ (f, g).2 e)) = if h : (f, g).2 = z then stinespringOp K (b, c) (f, g).1 * (a (f, g).1 d * e✝ (f, g).2 e) else onbPart hK (f, g) h (b, c) * (a (f, g).1 d * e✝ (f, g).2 e) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mg:Fin r⊢ g = z → ∀ (h : ¬g = z), stinespringOp K (b, c) f = onbPart hK (f, g) ⋯ (b, c) ∨ a f d = 0 ∨ e✝ g e = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mg:Fin rhg:g = z⊢ ∀ (h : ¬g = z), stinespringOp K (b, c) f = onbPart hK (f, g) ⋯ (b, c) ∨ a f d = 0 ∨ e✝ g e = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin m⊢ ∀ (h : ¬z = z), stinespringOp K (b, c) f = onbPart hK (f, z) ⋯ (b, c) ∨ a f d = 0 ∨ e✝ z e = 0 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rf:Fin mh:¬z = z⊢ stinespringOp K (b, c) f = onbPart hK (f, z) ⋯ (b, c) ∨ a f d = 0 ∨ e✝ z e = 0 All goals completed! 🐙 R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin r⊢ (if e = z then stinespringOp K (x✝, c) d else if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c)) = if h : e = z then stinespringOp K (x✝, c) d else onbPart hK (d, e) ⋯ (x✝, c) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:e = z⊢ stinespringOp K (x✝, c) d = stinespringOp K (x✝, c) dR:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:¬e = z⊢ onbPart hK (d, e) ⋯ (x✝, c) = onbPart hK (d, e) ⋯ (x✝, c) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:e = z⊢ stinespringOp K (x✝, c) d = stinespringOp K (x✝, c) dR:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin re✝:Matrix (Fin r) (Fin r) Ra:Matrix (Fin m) (Fin m) Rb:Fin mx✝:Fin mc:Fin rd:Fin me:Fin rg₀:¬e = z⊢ onbPart hK (d, e) ⋯ (x✝, c) = onbPart hK (d, e) ⋯ (x✝, c) All goals completed! 🐙

Note we don't need any special properties of M, and we don't need K to be CPTP.

Uses Fin types because of the use of Fin.sum_univ_succAbove in the proof.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ ∑ x_1, (∑ x_2 ∈ {x | x.2 = z} with z = x_2.2 ∧ z = (x_1, z).2, K x i x_2.1 * ρ x_2.1 (x_1, z).1 + ∑ x_2 ∈ {x | ¬x.2 = z} with z = x_2.2 ∧ z = (x_1, z).2, M (i, x) x_2 * ρ x_2.1 (x_1, z).1) * (starRingEnd R) (if (x_1, z).2 = z then K x j (x_1, z).1 else M (j, x) (x_1, z)) = ∑ x_1, (∑ j, K x i j * ρ j x_1) * (starRingEnd R) (K x j x_1)R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ Set.InjOn (fun y => (y, z)) ↑Finset.univ R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ ∑ x_1, (∑ x_2 ∈ {x | x.2 = z} with z = x_2.2 ∧ z = (x_1, z).2, K x i x_2.1 * ρ x_2.1 (x_1, z).1 + ∑ x_2 ∈ {x | ¬x.2 = z} with z = x_2.2 ∧ z = (x_1, z).2, M (i, x) x_2 * ρ x_2.1 (x_1, z).1) * (starRingEnd R) (if (x_1, z).2 = z then K x j (x_1, z).1 else M (j, x) (x_1, z)) = ∑ x_1, (∑ j, K x i j * ρ j x_1) * (starRingEnd R) (K x j x_1) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ ∑ x_1, ((∑ a, if a.2 = z then if z = a.2 then K x i a.1 * ρ a.1 x_1 else 0 else 0) + ∑ x_2, if x_2.2 = z then 0 else if z = x_2.2 then M (i, x) x_2 * ρ x_2.1 x_1 else 0) * (starRingEnd R) (K x j x_1) = ∑ x_1, (∑ j, K x i j * ρ j x_1) * (starRingEnd R) (K x j x_1); R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝¹:x ∈ Finset.univy:Fin mx✝:y ∈ Finset.univ⊢ ((∑ a, if a.2 = z then if z = a.2 then K x i a.1 * ρ a.1 y else 0 else 0) + ∑ x_1, if x_1.2 = z then 0 else if z = x_1.2 then M (i, x) x_1 * ρ x_1.1 y else 0) * (starRingEnd R) (K x j y) = (∑ j, K x i j * ρ j y) * (starRingEnd R) (K x j y) erw [ R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝¹:x ∈ Finset.univy:Fin mx✝:y ∈ Finset.univ⊢ ((∑ x_1, ∑ y_1, if (x_1, y_1).2 = z then if z = (x_1, y_1).2 then K x i (x_1, y_1).1 * ρ (x_1, y_1).1 y else 0 else 0) + ∑ x_1, if x_1.2 = z then 0 else if z = x_1.2 then M (i, x) x_1 * ρ x_1.1 y else 0) * (starRingEnd R) (K x j y) = (∑ j, K x i j * ρ j y) * (starRingEnd R) (K x j y) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝¹:x ∈ Finset.univy:Fin mx✝:y ∈ Finset.univ⊢ ((∑ x_1, ∑ y_1, if (x_1, y_1).2 = z then if z = (x_1, y_1).2 then K x i (x_1, y_1).1 * ρ (x_1, y_1).1 y else 0 else 0) + ∑ x_1, ∑ y_1, if (x_1, y_1).2 = z then 0 else if z = (x_1, y_1).2 then M (i, x) (x_1, y_1) * ρ (x_1, y_1).1 y else 0) * (starRingEnd R) (K x j y) = (∑ j, K x i j * ρ j y) * (starRingEnd R) (K x j y) R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝¹:x ∈ Finset.univy:Fin mx✝:y ∈ Finset.univ⊢ ((∑ x_1, ∑ y_1, if (x_1, y_1).2 = z then if z = (x_1, y_1).2 then K x i (x_1, y_1).1 * ρ (x_1, y_1).1 y else 0 else 0) + ∑ x_1, ∑ y_1, if (x_1, y_1).2 = z then 0 else if z = (x_1, y_1).2 then M (i, x) (x_1, y_1) * ρ (x_1, y_1).1 y else 0) * (starRingEnd R) (K x j y) = (∑ j, K x i j * ρ j y) * (starRingEnd R) (K x j y) All goals completed! 🐙; R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ Set.InjOn (fun y => (y, z)) ↑Finset.univ R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ Function.Injective fun y => (y, z); exact fun a b h => R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univa:Fin mb:Fin mh:(fun y => (y, z)) a = (fun y => (y, z)) b⊢ a = b All goals completed! 🐙; R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rz:Fin rM:Matrix (Fin m × Fin r) (Fin m × Fin r) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin mx:Fin rx✝:x ∈ Finset.univ⊢ ∀ x_1 ∈ Finset.univ, x_1 ∉ Finset.image (fun y => (y, z)) Finset.univ → (∑ x_2 ∈ {x | x.2 = z} with z = x_2.2 ∧ z = x_1.2, K x i x_2.1 * ρ x_2.1 x_1.1 + ∑ x_2 ∈ {x | ¬x.2 = z} with z = x_2.2 ∧ z = x_1.2, M (i, x) x_2 * ρ x_2.1 x_1.1) * (starRingEnd R) (if x_1.2 = z then K x j x_1.1 else M (j, x) x_1) = 0 All goals completed! 🐙

Notice that unitarity is a side property, it is not why the Stinespring form works.

Here z is the coordinate used for the ancilla.

All goals completed! 🐙

The "orthogonal" CPTP completion of a CPTNI map. Vtilde is an alternative name for krausCompletion.

def krausCompletion {R : Type*} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) : Matrix (Fin m × Fin (r+1)) (Fin m) R := fun x => dite (x.2 < r) (fun H => stinespringOp K ⟨x.1, ⟨x.2, H⟩⟩) fun _ => (CFC.sqrt (1 - (stinespringOp K)ᴴ * (stinespringOp K)) : Matrix _ _ _) x.1

Entrywise formula for the Stinespring isometry: its ((x₁, x₂), y) entry is K x₂ x₁ y.

theorem stinespringOp_apply {R : Type*} [Ring R] {m r : Type*} [Fintype r] [DecidableEq r] (K : r → Matrix m m R) (x : m × r) (y : m) : stinespringOp K x y = K x.2 x.1 y := R:Type u_1inst✝²:Ring Rm:Type u_2r:Type u_3inst✝¹:Fintype rinst✝:DecidableEq rK:r → Matrix m m Rx:m × ry:m⊢ stinespringOp K x y = K x.2 x.1 y R:Type u_1inst✝²:Ring Rm:Type u_2r:Type u_3inst✝¹:Fintype rinst✝:DecidableEq rK:r → Matrix m m Rx:m × ry:m⊢ (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0) = K x.2 x.1 y All goals completed! 🐙

The Gram matrix of the Stinespring isometry is ∑ i, (K i)ᴴ * K i.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Ra:Fin mb:Fin mi:Fin ra✝:i ∈ Finset.univ⊢ ∑ x, star (K (x, i).2 (x, i).1 a) * K (x, i).2 (x, i).1 b = ∑ j, star (K i) a j * K i j b R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Ra:Fin mb:Fin mi:Fin ra✝:i ∈ Finset.univ⊢ ∀ x ∈ Finset.univ, star (K (x, i).2 (x, i).1 a) * K (x, i).2 (x, i).1 b = star (K i) a x * K i x b R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Ra:Fin mb:Fin mi:Fin ra✝¹:i ∈ Finset.univx1:Fin ma✝:x1 ∈ Finset.univ⊢ star (K (x1, i).2 (x1, i).1 a) * K (x1, i).2 (x1, i).1 b = star (K i) a x1 * K i x1 b All goals completed! 🐙

Mar 14, 2026 by Bjørn for 4.27 June 13, 2026 by Aristotle for 4.31 including stinespringOp_gram and stinespringOp_apply.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, star K i * K i ≤ 1S:Matrix (Fin m × Fin r) (Fin m) R := stinespringOp KhS:S = stinespringOp Khgram:Sᴴ * S = ∑ i, star (K i) * K ih0:0 ≤ 1 - Sᴴ * SW:Matrix (Fin m) (Fin m) R := CFC.sqrt (1 - Sᴴ * S)hW:W = CFC.sqrt (1 - Sᴴ * S)hWsa:Wᴴ = WhWW:Wᴴ * W = 1 - Sᴴ * Shcast:∀ (x : Fin m) (i : Fin r) (c : Fin m), krausCompletion K (x, i.castSucc) c = S (x, i) chlast:∀ (x c : Fin m), krausCompletion K (x, Fin.last r) c = W x ckey:(krausCompletion K)ᴴ * krausCompletion K = Sᴴ * S + Wᴴ * W⊢ Sᴴ * S + (1 - Sᴴ * S) = 1 All goals completed! 🐙

A unital operator.

def unital {R : Type*} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) := ∑ i, K i * star (K i) = 1

A subunital operator.

def subunital {R : Type*} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) := ∑ i, K i * star (K i) ≤ 1

The identity Tr_B (A ⨂ B) = Tr(B) · A

R:Type u_1inst✝:RCLike Rm:ℕn:ℕA:Matrix (Fin m) (Fin m) RB:Matrix (Fin n) (Fin n) Ri:Fin mj:Fin mthis:(∑ i, B i i) * A i j = ∑ i_1, B i_1 i_1 * A i j⊢ ∑ x, A i j * B x x = ∑ i_1, B i_1 i_1 * A i j simp_rw R:Type u_1inst✝:RCLike Rm:ℕn:ℕA:Matrix (Fin m) (Fin m) RB:Matrix (Fin n) (Fin n) Ri:Fin mj:Fin mthis:(∑ i, B i i) * A i j = ∑ i_1, B i_1 i_1 * A i j⊢ ∑ x, A i j * B x x = ∑ i_1, B i_1 i_1 * A i jAll goals completed! 🐙]

A unitary dilation view of the application of a Kraus operator.

R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) RhK:∑ i, (K i)ᴴ * K i = 1z:Fin rρ:Matrix (Fin m) (Fin m) Rα:Matrix (Fin m) (Fin m) Rβ:Matrix (Fin r) (Fin r) Rhβ:β.trace = 1h:Ud hK z * kroneckerMap (fun x1 x2 => x1 * x2) ρ (single z z 1) * (Ud hK z)ᴴ = kroneckerMap (fun x1 x2 => x1 * x2) α β⊢ 1 • α = α All goals completed! 🐙

Trace of partial trace equals trace.

lemma trace_tr₂ {R : Type*} [RCLike R] {m n : ℕ} (ρ : Matrix (Fin m × Fin n) (Fin m × Fin n) R) : trace ρ = trace (tr₂ ρ) := Fintype.sum_prod_type fun x ↦ ρ x x

The Kraus completion as a map from operations to channels.

R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) RhK:QuantumOperation Kx:Fin qy:Fin q⊢ ∑ c, (((fun i x => krausCompletion K (x, i)) c)ᴴ * (fun i x => krausCompletion K (x, i)) c) x y = ∑ y_1, ∑ x_1, (krausCompletion K)ᴴ x (x_1, y_1) * krausCompletion K (x_1, y_1) y All goals completed! 🐙

The "not orthogonal" CPTP completion of a CPTNI map.

R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = True⊢ (fun x y => (∑ x, of fun i j => if x = i.2 ∧ 0 = j.2 then K x i.1 j.1 else 0) (x, ⟨↑i, ⋯⟩) (y, 0)) = K ⟨↑i, ⋯⟩ simp_rw R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = True⊢ (fun x y => (∑ x, of fun i j => if x = i.2 ∧ 0 = j.2 then K x i.1 j.1 else 0) (x, ⟨↑i, ⋯⟩) (y, 0)) = K ⟨↑i, ⋯⟩R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = True⊢ (fun x y => (∑ x, of fun i j => if x = i.2 ∧ True then K x i.1 j.1 else 0) (x, ⟨↑i, ⋯⟩) (y, 0)) = K ⟨↑i, ⋯⟩] R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = Truea:Fin qb:Fin q⊢ (∑ x, of fun i j => if x = i.2 ∧ True then K x i.1 j.1 else 0) (a, ⟨↑i, ⋯⟩) (b, 0) = K ⟨↑i, ⋯⟩ a b erw [R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = Truea:Fin qb:Fin q⊢ (∑ c, of (fun i j => if c = i.2 ∧ True then K c i.1 j.1 else 0) (a, ⟨↑i, ⋯⟩)) (b, 0) = K ⟨↑i, ⋯⟩ a bR:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = Truea:Fin qb:Fin q⊢ (∑ c, of (fun i j => if c = i.2 ∧ True then K c i.1 j.1 else 0) (a, ⟨↑i, ⋯⟩)) (b, 0) = K ⟨↑i, ⋯⟩ a b erw [R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = Truea:Fin qb:Fin q⊢ (fun a_1 => ∑ c, of (fun i j => if c = i.2 ∧ True then K c i.1 j.1 else 0) (a, ⟨↑i, ⋯⟩) a_1) (b, 0) = K ⟨↑i, ⋯⟩ a bR:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:↑i < rthis:∀ (j : Fin q × Fin 1), (0 = j.2) = Truea:Fin qb:Fin q⊢ (fun a_1 => ∑ c, of (fun i j => if c = i.2 ∧ True then K c i.1 j.1 else 0) (a, ⟨↑i, ⋯⟩) a_1) (b, 0) = K ⟨↑i, ⋯⟩ a b All goals completed! 🐙 R:Type u_1inst✝:RCLike Rq:ℕr:ℕK:Fin r → Matrix (Fin q) (Fin q) Rhq:QuantumOperation Ki:Fin (r + 1)H:¬i = Fin.last rg₀:¬↑i < r⊢ (fun x => CFC.sqrt (1 - (fun x y => (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0))ᴴ * fun x y => (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) x (y, 0)) x) = K ⟨↑i, ⋯⟩ All goals completed! 🐙

Partial trace on the left of a tensor product.

def partialTraceLeft {R : Type*} [RCLike R] {m n : Type*} [Fintype m] (ρ : Matrix (m × n) (m × n) R) : Matrix (n) (n) R := fun i j => ∑ k : m, ρ (k, i) (k, j)

A version of the Stinespring Dilation Theorem.

theorem stinespringForm_eq {R : Type*} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) (ρ : Matrix (Fin m) (Fin m) R) : tr₂ (stinespringDilation K ρ) = krausApply K ρ := R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rρ:Matrix (Fin m) (Fin m) R⊢ tr₂ (stinespringDilation K ρ) = krausApply K ρ R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rρ:Matrix (Fin m) (Fin m) R⊢ (fun i j => ∑ k, (stinespringOp K * ρ * (stinespringOp K)ᴴ) (i, k) (j, k)) = ∑ i, K i * ρ * (K i)ᴴ R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin m⊢ ∑ k, (stinespringOp K * ρ * (stinespringOp K)ᴴ) (i, k) (j, k) = (∑ i, K i * ρ * (K i)ᴴ) i j R:Type u_1inst✝:RCLike Rm:ℕr:ℕK:Fin r → Matrix (Fin m) (Fin m) Rρ:Matrix (Fin m) (Fin m) Ri:Fin mj:Fin m⊢ ∑ x, ∑ x_1, (∑ j, (∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) (i, x) (j, 0) * ρ j x_1) * (starRingEnd R) ((∑ i, kroneckerMap (fun x1 x2 => x1 * x2) (K i) (single i 0 1)) (j, x) (x_1, 0)) = (∑ i, K i * ρ * (K i)ᴴ) i j All goals completed! 🐙