Stinespring dilation

noncomputable def tr₂ {R : Type u_1} [Ring R] {m : Type u_2} {n : Type u_3} {m' : Type u_4} [Fintype n] (ρ : Matrix (m × n) (m' × n) R) : Matrix m m' R

Also known as partialTraceRight.

Equations

• tr₂ ρ i j = ∑ k : n, ρ (i, k) (j, k)

noncomputable def stinespringOp {R : Type u_1} [Ring R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) : Matrix (m × r) m R

stinespringOp is often written as V.

Equations

• stinespringOp K = fun (x : m × r) (y : m) => (∑ i : r, Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (K i) (Matrix.single i 0 1)) x (y, 0)

noncomputable def stinespringDilation {R : Type u_1} [Ring R] [StarRing R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (ρ : Matrix m m R) : Matrix (m × r) (m × r) R

Equations

• stinespringDilation K ρ = stinespringOp K * ρ * (stinespringOp K).conjTranspose

noncomputable def jlDilation {m r : ℕ} (K : Fin r.succ → Matrix (Fin m) (Fin m) ℂ) (ρ : Matrix (Fin m) (Fin m) ℂ) : Matrix (Fin m × Fin r.succ) (Fin m × Fin r.succ) ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def jDilation {m r : ℕ} (K : Fin r.succ → Matrix (Fin m) (Fin m) ℂ) (ρ : Matrix (Fin m) (Fin m) ℂ) : Matrix (Fin m × Fin (r + 1)) (Fin m × Fin (r + 1)) ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem jDilation₃ (K : Fin 3 → Matrix (Fin 1) (Fin 1) ℂ) (ρ : Matrix (Fin 1) (Fin 1) ℂ) : tr₂ (jDilation K ρ) = K 0 * ρ * (K 0).conjTranspose + K 1 * ρ * (K 1).conjTranspose

theorem jDilation₂ (K : Fin 2 → Matrix (Fin 1) (Fin 1) ℂ) (ρ : Matrix (Fin 1) (Fin 1) ℂ) : tr₂ (jlDilation K ρ) = K 0 * ρ * (K 0).conjTranspose

noncomputable def stinespringForm {R : Type u_1} [Ring R] [StarRing R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (ρ : Matrix m m R) : Matrix m m R

Equations

• stinespringForm K ρ = tr₂ (stinespringDilation K ρ)

theorem stinespringOp_adjoint_mul_self {R : Type u_1} [Ring R] [StarRing R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) : ∑ i : r, star K i * K i = (stinespringOp K).conjTranspose * stinespringOp K

theorem stinespringForm_CPTNI {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (hK : ∑ i : r, (K i).conjTranspose * K i ≤ 1) : (stinespringOp K).conjTranspose * stinespringOp K ≤ 1

theorem stinespringForm_CPTP_isometry {R : Type u_1} [Ring R] [StarRing R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] {K : r → Matrix m m R} (hK : ∑ i : r, (K i).conjTranspose * K i = 1) : (stinespringOp K).conjTranspose * stinespringOp K = 1

theorem hzRC {R : Type u_1} [RCLike R] (z : R) : star z * z = ↑‖z‖ ^ 2

theorem stinespringOrtho {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] {K : r → Matrix m m R} (hK : ∑ i : r, (K i).conjTranspose * K i = 1) : Orthonormal R fun (j : m) => WithLp.toLp 2 fun (i : m × r) => stinespringOp K i j

Mar 16, 2026 (Mar 27: RCLike version) Proving the columns of V = stinespringOp K are independent is a step on the way to constructing the unitary dilation.

theorem basisCard {R : Type u_1} [RCLike R] {n : Type u_2} {m : Type u_3} [Fintype n] {s : Matrix n m R} (ho : Orthonormal R fun (j : m) => WithLp.toLp 2 fun (i : n) => s i j) : Fintype.card n = ⋯.choose.card

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

theorem stinespringCard {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] {K : r → Matrix m m R} (hK : ∑ i : r, (K i).conjTranspose * K i = 1) : Fintype.card (m × r) = ⋯.choose.card

theorem complCard {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : have 𝓞 := fun (j : Fin m) => WithLp.toLp 2 fun (i : Fin m × Fin r) => stinespringOp K i j; have theRange := Submodule.span R (Set.range 𝓞); have u' := ⋯.choose; Fintype.card (Fin m × Fin (r - 1)) = u'.card

We need the 1 matrix, which we don't seem to have for an arbitrary [Fintype m]. Since we are comparing Fin r and Fin (r-1) we also cannot too easily use an arbitrary [Fintype r] [Zero r].

def Fin.predAbove_of_ne {n : ℕ} {k i : Fin n} (h : i ≠ k) : Fin (n - 1)

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

Equations

• Fin.predAbove_of_ne h = if H : ↑i > ↑k then ⟨↑i - 1, ⋯⟩ else ⟨↑i, ⋯⟩

theorem Fin.predAbove_of_ne_injective (n : ℕ) (k x y : Fin n) (hx : x ≠ k) (hy : y ≠ k) (heq : predAbove_of_ne hx = predAbove_of_ne hy) : x = y

noncomputable def onbPart {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (x : Fin m × Fin r) {z : Fin r} (hx : ¬x.2 = z) : Fin m × Fin r → R

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

Equations

• onbPart hK x hx = (fun (w : Fin m × Fin (r - 1)) => (↑(⋯.choose ((Finset.equivOfCardEq ⋯) ⟨w, ⋯⟩))).ofLp) (x.1, Fin.predAbove_of_ne hx)

theorem onbPart_inner {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) {z : Fin r} {y : Fin m × Fin r} (hy : ¬y.2 = z) {x : Fin m × Fin r} (hx : ¬x.2 = z) (h : y ≠ x) : inner R (WithLp.toLp 2 (onbPart hK y hy)) (WithLp.toLp 2 (onbPart hK x hx)) = 0

theorem onbPart_norm {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (x : Fin m × Fin r) {z : Fin r} (hx : ¬x.2 = z) : ‖WithLp.toLp 2 (onbPart hK x hx)‖ = 1

noncomputable def Ud {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : Matrix (Fin m × Fin r) (Fin m × Fin r) R

Also known as unitaryDilation. Respects x,y order.

Equations

• Ud hK z x y = if hy : y.2 = z then stinespringOp K x y.1 else onbPart hK y hy x

noncomputable def dilation {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (z : r) (M : Matrix (m × r) (m × r) R) : Matrix (m × r) (m × r) R

A general, not necessarily unitary, dilation.

Equations

• dilation K z M x y = if y.2 = z then stinespringOp K x y.1 else M x y

theorem Ud_orthonormal₁ {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : Orthonormal R fun (y : Fin m × Fin r) => if hy : y.2 = z then WithLp.toLp 2 fun (i : Fin m × Fin r) => stinespringOp K i y.1 else WithLp.toLp 2 fun (i : Fin m × Fin r) => onbPart hK y hy i

One version of it.

theorem Ud_orthonormal₂ {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : Orthonormal R fun (y : Fin m × Fin r) => WithLp.toLp 2 fun (i : Fin m × Fin r) => if hy : y.2 = z then stinespringOp K i y.1 else onbPart hK y hy i

theorem RCLike.norm_eq {R : Type u_1} [RCLike R] (γ : R) : re γ * re γ + im γ * im γ = ‖γ‖ ^ 2

theorem smul_self_one_of_norm_one {R : Type u_1} [RCLike R] {t : Type u_2} [Fintype t] {β : t → R} (hj : ‖WithLp.toLp 2 β‖ = 1) : ∑ x : t, (starRingEnd R) (β x) * β x = 1

theorem unitary_of_orthonormal {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (α : Matrix (m × r) (m × r) R) (h₀ : Orthonormal R fun (i : m × r) => WithLp.toLp 2 (α i)) : α * star α = 1

theorem Ud_unitaryT {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : (Ud hK z).transpose ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)

theorem Ud_unitary {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : Ud hK z ∈ unitary (Matrix (Fin m × Fin r) (Fin m × Fin r) R)

Well will you look at that...

def e₀Xe₀ {R : Type u_1} [RCLike R] {w : Type u_2} [Fintype w] [DecidableEq w] [Zero w] : Matrix w w R

Equations

• e₀Xe₀ x y = if (x, y) = (0, 0) then 1 else 0

theorem tr₂_e₀Xe₀ {R : Type u_1} [RCLike R] {m : Type u_2} {w : Type u_3} [Fintype w] [Zero w] (e : Matrix w w R) (htr : e.trace = 1) (ρ : Matrix m m R) : tr₂ (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ e) = ρ

Does not need (he : e = e₀Xe₀).

noncomputable def stinespringUnitaryForm {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) (ρ : Matrix (Fin m) (Fin m) R) : Matrix (Fin m) (Fin m) R

The best version.

Equations

• stinespringUnitaryForm hK z ρ = tr₂ (Ud hK z * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ (Matrix.single z z 1) * (Ud hK z).conjTranspose)

noncomputable def stinespringUnitaryForm_e {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * 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

Equations

• stinespringUnitaryForm_e hK z e ρ = tr₂ (Ud hK z * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ e * (Ud hK z).conjTranspose)

noncomputable def UdWord {α : Type u_1} {R : Type u_2} [RCLike R] {n q r : ℕ} {𝓚 : α → Fin r → Matrix (Fin q) (Fin q) R} (hK : ∀ (s : α), ∑ i : Fin r, (𝓚 s i).conjTranspose * 𝓚 s i = 1) (z : Fin r) (word : Fin n → α) (ρ : Matrix (Fin q × Fin r) (Fin q × Fin r) R) : Matrix (Fin q × Fin r) (Fin q × Fin r) R

Unitary dilation, processing a whole word

theorem tracefree_version {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Zero r] [Fintype m] [DecidableEq m] {K : r → Matrix m m R} (ρ : Matrix m m R) : have K' := fun (i : r) (x y : m) => star (K i y x); have U := stinespringOp K'; U.conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ 1 * U = stinespringForm K ρ

theorem heisenberg_schrõdinger {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Zero r] [Fintype m] [DecidableEq m] {K : r → Matrix m m R} (ρ : Matrix m m R) : have K' := fun (i : r) (x y : m) => star (K i y x); have U := stinespringOp K'; have V := stinespringOp K; have schrõdinger := tr₂ (V * ρ * V.conjTranspose); have heisenberg := U.conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ 1 * U; schrõdinger = heisenberg

noncomputable def stinespringGeneralForm {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (z : r) (M : Matrix (m × r) (m × r) R) (ρ : Matrix m m R) : Matrix m m R

Equations

• stinespringGeneralForm K z M = fun (ρ : Matrix m m R) => tr₂ (dilation K z M * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ (Matrix.single z z 1) * (dilation K z M).conjTranspose)

noncomputable def stinespringGeneralForm_e {R : Type u_1} [RCLike R] {m : Type u_2} {r : Type u_3} [Fintype r] [DecidableEq r] [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (z : r) (e : Matrix r r R) (M : Matrix (m × r) (m × r) R) (ρ : Matrix m m R) : Matrix m m R

Equations

• stinespringGeneralForm_e K z e M = fun (ρ : Matrix m m R) => tr₂ (dilation K z M * Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ρ e * (dilation K z M).conjTranspose)

theorem unitaryForm_of_general {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : stinespringGeneralForm K z (Ud hK z) = stinespringUnitaryForm hK z

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

theorem unitaryForm_of_general_e {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) (e : Matrix (Fin r) (Fin r) R) : stinespringGeneralForm_e K z e (Ud hK z) = stinespringUnitaryForm_e hK z e

theorem stinespringGeneralForm_works {R : Type u_1} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) (z : Fin r) (M : Matrix (Fin m × Fin r) (Fin m × Fin r) R) : stinespringGeneralForm K z M = krausApply K

Mar 26, 2026 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.

theorem stinespringUnitaryForm_works {R : Type u_1} [RCLike R] {m r : ℕ} {K : Fin r → Matrix (Fin m) (Fin m) R} (hK : ∑ i : Fin r, (K i).conjTranspose * K i = 1) (z : Fin r) : stinespringUnitaryForm hK z = krausApply K

Mar 25, 2026 Behold...

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

Here z is the coordinate used for the ancilla.

noncomputable def krausCompletion {R : Type u_1} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) : Matrix (Fin m × Fin (r + 1)) (Fin m) R

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

Equations

• krausCompletion K x = if H : ↑x.2 < r then stinespringOp K (x.1, ⟨↑x.2, H⟩) else CFC.sqrt (1 - (stinespringOp K).conjTranspose * stinespringOp K) x.1

theorem krausCompletion_isometry_of_TNI {R : Type u_1} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) (h_tni : ∑ i : Fin r, star K i * K i ≤ 1) : (krausCompletion K).conjTranspose * krausCompletion K = 1

Mar 14, 2026

def unital {R : Type u_1} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) : Prop

Equations

• unital K = (∑ i : Fin r, K i * star (K i) = 1)

def subunital {R : Type u_1} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) : Prop

Equations

• subunital K = (∑ i : Fin r, K i * star (K i) ≤ 1)

theorem Matrix.mul_comm_one {R : Type u_1} [RCLike R] (A B : Matrix (Fin 1) (Fin 1) R) : A * B = B * A

theorem krausCompletion_I₂ₘNEWPROOF {r : ℕ} (K : Fin r → Matrix (Fin 1) (Fin 1) ℂ) (h_unital : subunital K) : (krausCompletion K).conjTranspose * krausCompletion K = 1

theorem krausCompletion_isometry_of_zero {m : ℕ} (K : Fin 0 → Matrix (Fin m) (Fin m) ℂ) : (krausCompletion K).conjTranspose * krausCompletion K = 1

krausCompletion is an isometry when r=0

theorem krausCompletion_Iᵣ₀ {r : ℕ} (K : Fin r → Matrix (Fin 0) (Fin 0) ℂ) : (krausCompletion K).conjTranspose * krausCompletion K = 1

krausCompletion is an isometry when m=0

theorem partialTrace_tensor {R : Type u_1} [RCLike R] {m n : ℕ} (A : Matrix (Fin m) (Fin m) R) (B : Matrix (Fin n) (Fin n) R) : tr₂ (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B) = B.trace • A

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

theorem trace_tr₂ {R : Type u_1} [RCLike R] {m n : ℕ} (ρ : Matrix (Fin m × Fin n) (Fin m × Fin n) R) : ρ.trace = (tr₂ ρ).trace

theorem CPTP_of_CPTNI {R : Type u_1} [RCLike R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hq : quantumOperation K) : ∃ (K' : Fin (r + 1) → Matrix (Fin q) (Fin q) R), quantumChannel K' ∧ ∀ (i : Fin (r + 1)) (H : i ≠ Fin.last r), K' i = K ⟨↑i, ⋯⟩

Feb 2, 2026 The "not orthogonal" CPTP completion of a CPTNI map.

noncomputable def partialTraceLeft {R : Type u_1} [RCLike R] {m n : ℕ} (ρ : Matrix (Fin m × Fin n) (Fin m × Fin n) R) : Matrix (Fin n) (Fin n) R

Equations

• partialTraceLeft ρ i j = ∑ k : Fin m, ρ (k, i) (k, j)