Kraus operator automata and projection-valued measures

We define the language accepted by a measure-once Kraus operator automaton, and a family of examples due to Grudka et al.

References:

• S. Lakshmanan, Finite-State Quantum Computational Complexity, doctoral dissertation, University of Hawaii at Manoa, 2026.

• Quantum Synchronizing Words: Resetting and Preparing Qutrit States, Grudka et al., 2025

• Unbounded length minimal synchronizing words for quantum channels over qutrits, B. Kjos-Hanssen and J. Lakshmanan, QCNC 2026.

def krausApply {R : Type u_1} [Mul R] [Star R] [AddCommMonoid R] {q : Type u_2} {r : Type u_3} [Fintype q] [Fintype r] [DecidableEq q] [DecidableEq r] (K : r → Matrix q q R) (ρ : Matrix q q R) : Matrix q q R

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

Equations

• krausApply K ρ = ∑ i : r, K i * ρ * (K i).conjTranspose

theorem krausApply.posSemidef {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {q : Type u_2} {r : Type u_3} [Fintype q] [Fintype r] [DecidableEq q] [DecidableEq r] (K : r → Matrix q q R) {ρ : Matrix q q R} (hρ : ρ.PosSemidef) : (krausApply K ρ).PosSemidef

Kraus operator preserves PSD property.

def QuantumChannel {R : Type u_1} [Mul R] [One R] [Star R] [AddCommMonoid R] {q : Type u_2} {r : Type u_3} [Fintype q] [Fintype r] [DecidableEq q] [DecidableEq r] (K : r → Matrix q q R) : Prop

Equations

• QuantumChannel K = (∑ i : r, (K i).conjTranspose * K i = 1)

def QuantumOperation {R : Type u_1} [RCLike R] {q : Type u_2} {r : Type u_3} [Fintype q] [Fintype r] [DecidableEq q] [DecidableEq r] (K : r → Matrix q q R) : Prop

Equations

• QuantumOperation K = (∑ i : r, (K i).conjTranspose * K i ≤ 1)

def densityMatrix {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] (d : Type u_2) [Fintype d] : Type (max 0 u_1 u_2)

Equations

• densityMatrix d = { ρ : Matrix d d R // ρ.PosSemidef ∧ ρ.trace = 1 }

def densityMatrix.convex_comb {R : Type u_1} [RCLike R] {d : ℕ} (ρ₀ ρ₁ : densityMatrix (Fin d)) {t : R} (hp₀ : 0 ≤ t) (hp₁ : 0 ≤ 1 - t) : densityMatrix (Fin d)

Equations

• ρ₀.convex_comb ρ₁ hp₀ hp₁ = ⟨t • ↑ρ₀ + (1 - t) • ↑ρ₁, ⋯⟩

def subNormalizedDensityMatrix {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] (q : Type u_2) [Fintype q] : Type (max 0 u_1 u_2)

Equations

• subNormalizedDensityMatrix q = { ρ : Matrix q q R // ρ.PosSemidef ∧ ρ.trace ≤ 1 }

theorem QuantumChannel.trace_eq {R : Type u_1} [CommRing R] [PartialOrder R] [StarRing R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hK : QuantumChannel K) (ρ : Matrix (Fin q) (Fin q) R) : (krausApply K ρ).trace = ρ.trace

theorem QuantumChannel.trace_eq_one {R : Type u_1} [CommRing R] [PartialOrder R] [StarRing R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hK : QuantumChannel K) (ρ : Matrix (Fin q) (Fin q) R) (hρ : ρ.trace = 1) : (krausApply K ρ).trace = 1

def densityMatrix.applyChannel {R : Type u_1} [CommRing R] [PartialOrder R] [StarRing R] [AddLeftMono R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hK : QuantumChannel K) (ρ : densityMatrix (Fin q)) : densityMatrix (Fin q)

Realizing a QuantumChannel as a map on densityMatrices.

Equations

• densityMatrix.applyChannel hK ρ = ⟨krausApply K ↑ρ, ⋯⟩

def krausApplyWord {α : Type u_1} {R : Type u_2} [Mul R] [Star R] [AddCommMonoid R] {n q r : ℕ} (word : Fin n → α) (𝓚 : α → Fin r → Matrix (Fin q) (Fin q) R) (ρ : Matrix (Fin q) (Fin q) R) : Matrix (Fin q) (Fin q) R

Transition function δ^* corresponding to a word word over an alphabet α, where each symbol a:α is mapped to a completely positive map in Kraus form, of rank at most r.

Equations

• krausApplyWord word_2 𝓚 ρ = ρ
• krausApplyWord word_2 𝓚 ρ = krausApply (𝓚 (word_2 (Fin.last m))) (krausApplyWord (Fin.init word_2) 𝓚 ρ)

theorem krausApplyWord_densityMatrix {α : Type u_1} {R : Type u_2} [CommRing R] [StarRing R] [PartialOrder R] [AddLeftMono R] {n q r : ℕ} (word : Fin n → α) {𝓚 : α → Fin r → Matrix (Fin q) (Fin q) R} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) (ρ : densityMatrix (Fin q)) : (krausApplyWord word 𝓚 ↑ρ).PosSemidef ∧ (krausApplyWord word 𝓚 ↑ρ).trace = 1

Using a family of quantum channels, we can iterate over a word and stay within the density matrices.

def krausApplyWord_map {α : Type u_1} {R : Type u_2} [CommRing R] [StarRing R] [PartialOrder R] [AddLeftMono R] {n q r : ℕ} (word : Fin n → α) (𝓚 : α → Fin r → Matrix (Fin q) (Fin q) R) (hq : ∀ (a : α), QuantumChannel (𝓚 a)) (ρ : densityMatrix (Fin q)) : densityMatrix (Fin q)

Using a family of quantum channels, we can iterate over a word and stay within the density matrices.

Equations

• krausApplyWord_map word 𝓚 hq ρ = ⟨krausApplyWord word 𝓚 ↑ρ, ⋯⟩

def e {R : Type u_1} [One R] [Zero R] {k : Type u_2} [DecidableEq k] : k → Matrix k (Fin 1) R

Equations

• e i = Matrix.single i 0 1

def ev {R : Type u_1} [One R] [Zero R] {k : ℕ} : Fin k → Fin k → R

A version of e for use with *ᵥ. However, when combining with ⊗ₖ it may be better to stick with e.

Equations

• ev i j = if i = j then 1 else 0

def pureState_C {R : Type u_1} [Mul R] [Add R] [Zero R] [Star R] {k : ℕ} (e : Matrix (Fin k) (Fin 1) R) : Matrix (Fin k) (Fin k) R

Equations

• pureState_C e = e.mulᵣ e.conjTranspose

def pureState' {R : Type u_1} [RCLike R] {k : Type u_2} {l : Type u_3} [Fintype k] [Fintype l] (v : Matrix k l R) : Matrix k k R

Equations

• pureState' v = v * v.conjTranspose

def pureState_Cv {R : Type u_1} [Mul R] [Add R] [Zero R] [Star R] {k : ℕ} (e : Fin k → R) : Matrix (Fin k) (Fin k) R

A version of pureState_C for use with *ᵥ.

Equations

• pureState_Cv e i j = e i * star e j

theorem preState_Cv_eq_pureState_C {R : Type u_1} [Mul R] [Add R] [Zero R] [Star R] {k : ℕ} (e : Matrix (Fin k) (Fin 1) R) : pureState_C e = pureState_Cv fun (i : Fin k) => e i 0

theorem pureState_selfAdjoint_C {R : Type u_1} [Ring R] [StarRing R] {k : ℕ} (e : Matrix (Fin k) (Fin 1) R) : (pureState_C e).IsHermitian

def pureState_projection'_C {R : Type u_1} [RCLike R] {k : ℕ} (e : EuclideanSpace R (Fin k)) (he : ‖e‖ = 1) : IsStarProjection (pureState_C fun (i : Fin k) (x : Fin 1) => e.ofLp i)

Equations

• ⋯ = ⋯

theorem pureState_projection_C {R : Type u_1} [Ring R] [StarRing R] {k : ℕ} (i : Fin k) : IsStarProjection (pureState_C (e i))

theorem pureState_projection''_C {R : Type u_1} [RCLike R] : IsStarProjection (pureState_C (e 0) + pureState_C (e 1))

theorem psd_versions_general {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {k : ℕ} {e : Matrix (Fin k) (Fin k) R} {x : Fin k →₀ R} (he : 0 ≤ star ⇑x ⬝ᵥ e.mulVec ⇑x) : 0 ≤ x.sum fun (i : Fin k) (xi : R) => x.sum fun (j : Fin k) (xj : R) => star xi * e i j * xj

theorem psd_versions {k : ℕ} {e : Matrix (Fin k) (Fin k) ℝ} {x : Fin k →₀ ℝ} (he : 0 ≤ ⇑x ⬝ᵥ e.mulVec ⇑x) : 0 ≤ x.sum fun (i : Fin k) (xi : ℝ) => x.sum fun (j : Fin k) (xj : ℝ) => star xi * e i j * xj

theorem dotProduct_mul_mulVec {R : Type u_1} [RCLike R] (k : ℕ) (d : Matrix (Fin k) (Fin 1) R) (e : Matrix (Fin 1) (Fin k) R) (α β : Fin k → R) : β ⬝ᵥ (d * e).mulVec α = (Matrix.vecMul β d * e.mulVec α) 0

theorem pureState_psd_C {R : Type u_1} [RCLike R] [PartialOrder R] [StarOrderedRing R] {k : ℕ} (e : Matrix (Fin k) (Fin 1) R) : (pureState_C e).PosSemidef

theorem pure_state_eq {k : ℕ} (i : Fin k) : (Matrix.single i 0 1).mulᵣ (Matrix.single i 0 1).transpose = Matrix.single i i 1

theorem pure_state_eq_C {R : Type u_1} [RCLike R] {k : ℕ} (i : Fin k) : (Matrix.single i 0 1).mulᵣ (Matrix.single i 0 1).conjTranspose = Matrix.single i i 1

theorem matrix_caution : (fun (x x_1 : Fin 2) => 1) = 1

Cautionary example: This does not become a matrix! A different kind of identity kicks in.

@[implicit_reducible]

noncomputable instance instNormedRingMatrixFinOfNatNatComplex_kraus : NormedRing (Matrix (Fin 2) (Fin 2) ℂ)

Equations

• instNormedRingMatrixFinOfNatNatComplex_kraus = Matrix.frobeniusNormedRing

@[implicit_reducible]

noncomputable instance instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus : NormedAlgebra ℝ (Matrix (Fin 2) (Fin 2) ℂ)

Equations

• instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus = Matrix.frobeniusNormedAlgebra

theorem oftr {n : ℕ} (P : Matrix (Fin n) (Fin n) ℝ) (hP : 0 ≤ P) : 0 ≤ P.transpose

theorem matrix_posSemidef_eq_star_mul_self'_C {R : Type u_1} [RCLike R] {n : ℕ} (P : Matrix (Fin n) (Fin n) R) (hP : 0 ≤ P) : ∃ (B : Matrix (Fin n) (Fin n) R), P = star B * B

theorem trace_mul_posSemidef_nonneg {n : ℕ} {ρ P : Matrix (Fin n) (Fin n) ℝ} (hρ : ρ.PosSemidef) (hP : P.PosSemidef) : 0 ≤ (P * ρ).trace

theorem trace_mul_posSemidef_nonneg_general {R : Type u_1} [RCLike R] {n : ℕ} {ρ P : Matrix (Fin n) (Fin n) R} (hρ : ρ ≥ 0) (hP : P ≥ 0) : 0 ≤ (P * ρ).trace

theorem QuantumOperation.trace_le {R : Type u_1} [RCLike R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hK : QuantumOperation K) {ρ : Matrix (Fin q) (Fin q) R} (hρ : 0 ≤ ρ) : (krausApply K ρ).trace ≤ ρ.trace

Feb 1, 2026. And almost again May 9, 2026.

theorem QuantumOperation_preserves_trace_le_one {R : Type u_1} [RCLike R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hK : QuantumOperation K) {ρ : Matrix (Fin q) (Fin q) R} (hρ : 0 ≤ ρ) (hρ₁ : ρ.trace ≤ 1) : (krausApply K ρ).trace ≤ 1

def krausApply_subNormalizedDensityMatrix {R : Type u_1} [RCLike R] {q r : ℕ} {K : Fin r → Matrix (Fin q) (Fin q) R} (hK : QuantumOperation K) (ρ : subNormalizedDensityMatrix (Fin q)) : subNormalizedDensityMatrix (Fin q)

Feb 1, 2026 Realizing a QuantumOperation as a map on subnormalized density matrices.

Equations

• krausApply_subNormalizedDensityMatrix hK ρ = ⟨krausApply K ↑ρ, ⋯⟩

theorem krausApplyWord_subNormalizedDensityMatrix {α : Type u_1} {R : Type u_2} [RCLike R] {n q r : ℕ} (word : Fin n → α) {𝓚 : α → Fin r → Matrix (Fin q) (Fin q) R} (h𝓚 : ∀ (a : α), QuantumOperation (𝓚 a)) (ρ : subNormalizedDensityMatrix (Fin q)) : (krausApplyWord word 𝓚 ↑ρ).PosSemidef ∧ (krausApplyWord word 𝓚 ↑ρ).trace ≤ 1

def krausApplyWord_map_sub {α : Type u_1} {R : Type u_2} [RCLike R] {n q r : ℕ} (word : Fin n → α) {𝓚 : α → Fin r → Matrix (Fin q) (Fin q) R} (h𝓚 : ∀ (a : α), QuantumOperation (𝓚 a)) (ρ : subNormalizedDensityMatrix (Fin q)) : subNormalizedDensityMatrix (Fin q)

If each letter is a quantum channel then the whole word maps density matrices to density matrices.

Equations

• krausApplyWord_map_sub word h𝓚 ρ = ⟨krausApplyWord word 𝓚 ↑ρ, ⋯⟩

theorem posSemidef_of_isStarProjection {n : ℕ} (P : Matrix (Fin n) (Fin n) ℝ) (hP : IsStarProjection P) : P.PosSemidef

theorem posSemidef_of_isStarProjection_C {R : Type u_1} [RCLike R] {n : ℕ} (P : Matrix (Fin n) (Fin n) R) (hP : IsStarProjection P) : P.PosSemidef

theorem trace_mul_nonneg {n : ℕ} {ρ P : Matrix (Fin n) (Fin n) ℝ} (hρ' : ρ.PosSemidef) (hP : IsStarProjection P) : 0 ≤ (P * ρ).trace

theorem trace_mul_nonneg_C {R : Type u_1} [RCLike R] {n : ℕ} {ρ P : Matrix (Fin n) (Fin n) R} (hρ' : ρ.PosSemidef) (hP : IsStarProjection P) : 0 ≤ (P * ρ).trace

theorem nonneg_trace'_C {R : Type u_1} [RCLike R] {n : ℕ} {ρ : Matrix (Fin n) (Fin n) R} (hρ' : ρ.PosSemidef) (e : Matrix (Fin n) (Fin 1) R) (he : ‖WithLp.toLp 2 fun (i : Fin n) => e i 0‖ = 1) : 0 ≤ (pureState_C e * ρ).trace

theorem nonneg_trace_of_posSemidef_C {R : Type u_1} [RCLike R] {n : ℕ} {ρ : Matrix (Fin n) (Fin n) R} (hρ' : ρ.PosSemidef) (i : Fin n) : 0 ≤ (pureState_C (e i) * ρ).trace

theorem sum_rows_C {R : Type u_1} [RCLike R] {k : ℕ} (ρ : Matrix (Fin k) (Fin k) R) : ∑ x : Fin k, Matrix.of (Function.update 0 x (ρ.row x)) = ρ

theorem single_row {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (x : Fin k) : Matrix.single x x 1 * ρ = Matrix.of (Function.update 0 x (ρ.row x))

theorem combined_rows {k : ℕ} (ρ : Matrix (Fin k) (Fin k) ℝ) : ∑ x : Fin k, Matrix.single x x 1 * ρ = ρ

theorem standard_basis_probability_C {R : Type u_1} [RCLike R] {k : ℕ} (ρ : Matrix (Fin k) (Fin k) R) : ∑ a : Fin k, (pureState_C (e a) * ρ).trace = ρ.trace

Unlike standard_basis_probability_one this one does not require PSD.

theorem standard_basis_probability_one_C {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) : ∑ a : Fin k, (pureState_C (e a) * ρ).trace = 1

Unlike standard_basis_probability_one this one does not require PSD.

theorem standard_basis_probability_le_one_C {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) : ∑ a : Fin k, (pureState_C (e a) * ρ).trace ≤ 1

Unlike standard_basis_probability_one this one does not require PSD.

theorem standard_basis_probability_general {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} : ∑ a : Fin k, (pureState_C (e a) * ρ).trace = ρ.trace

def subPMF (α : Type u_1) : Type u_1

Equations

• subPMF α = { f : α → ENNReal // ∃ p ≤ 1, HasSum f p }

def subPMF.ofFinset (α : Type u_1) (f : α → ENNReal) (s : Finset α) (h : ∑ a ∈ s, f a ≤ 1) (h' : ∀ a ∉ s, f a = 0) : subPMF α

Equations

• subPMF.ofFinset α f s h h' = ⟨f, ⋯⟩

def subPMF.ofFintype (α : Type u_1) [Fintype α] (f : α → ENNReal) (h : ∑ a : α, f a ≤ 1) : subPMF α

Equations

• subPMF.ofFintype α f h = (fun (f : α → ENNReal) => subPMF.ofFinset α f Finset.univ) f h ⋯

theorem one_eq_sum_pureState {R : Type u_1} [RCLike R] {k : ℕ} : ∑ i : Fin k, pureState_C (e i) = 1

theorem sum_one_sub₀ {R : Type u_1} [Ring R] {k : ℕ} (acc : Fin k) (f : Fin k → Matrix (Fin k) (Fin k) R) : ∑ i : Fin k, f i - f acc = ∑ i : Fin k, if i = acc then 0 else f i

theorem trace_one_sub_C {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hPS : ρ.PosSemidef) : 0 ≤ ((1 - pureState_C (e acc)) * ρ).trace

theorem pure_trace_one_sub_re {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hPS : ρ.PosSemidef) : 0 ≤ RCLike.re ((1 - pureState_C (e acc)) * ρ).trace

theorem pure_trace_nonneg_re {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hPS : ρ.PosSemidef) : 0 ≤ RCLike.re (pureState_C (e acc) * ρ).trace

def preQuantumInstrument {R : Type u_1} [RCLike R] {q : Type u_2} {r : Type u_3} [Fintype q] [Fintype r] [DecidableEq q] [DecidableEq r] {α : Type u_4} [Fintype α] (𝓔 : α → r → Matrix q q R) : Prop

Equations

• preQuantumInstrument 𝓔 = ∀ ρ ≥ 0, (∑ i : α, krausApply (𝓔 i) ρ).trace = ρ.trace

def QuantumInstrument {R : Type u_1} [RCLike R] {q : Type u_2} {r : Type u_3} [Fintype q] [Fintype r] [DecidableEq q] [DecidableEq r] {α : Type u_4} [Fintype α] (𝓔 : α → r → Matrix q q R) : Prop

Equations

• QuantumInstrument 𝓔 = (preQuantumInstrument 𝓔 ∧ ∀ (a : α), ∑ i : r, (𝓔 a i).conjTranspose * 𝓔 a i ≤ 1)

theorem ofReal_inj_aux {α : Type u_1} [Fintype α] {J : α → ℝ} (hnn : ∀ (a : α), J a ≥ 0) : ∑ a : α, ⟨J a, ⋯⟩ = ⟨∑ a : α, J a, ⋯⟩

theorem krausApply_trace_nonneg {R : Type u_1} [RCLike R] {r : Type u_2} [Fintype r] [inst_2 : DecidableEq r] {α : Type u_3} {k : ℕ} {𝓔 : α → r → Matrix (Fin k) (Fin k) R} {ρ : Matrix (Fin k) (Fin k) R} (hPS : 0 ≤ ρ) (i : α) : 0 ≤ (krausApply (𝓔 i) ρ).trace

def PMF_of_preQuantumInstrument {R : Type u_1} [RCLike R] {r : Type u_2} [Fintype r] [DecidableEq r] {α : Type u_3} [Fintype α] {k : ℕ} {𝓔 : α → r → Matrix (Fin k) (Fin k) R} (h𝓔 : preQuantumInstrument 𝓔) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : 0 ≤ ρ) : PMF α

May 13, 2026.

Equations

• PMF_of_preQuantumInstrument h𝓔 hUT hPS = PMF.ofFintype (fun (i : α) => ↑⟨RCLike.re (krausApply (𝓔 i) ρ).trace, ⋯⟩) ⋯

theorem pureState_C_QuantumInstrument {R : Type u_1} [RCLike R] {q : ℕ} : QuantumInstrument fun (i : Fin q) (x : Fin 1) => pureState_C (e i)

def POVM_PMF {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : 0 ≤ ρ) : PMF (Fin k)

Positive operator (or projection) valued measure as a probability mass function. Technically the measure is valued in Fin k although pureState (e i) can stand for i. Could be generalized to let e be any orthonormal basis.

pureState_psd shows that it is a POVM. pureState_projection shows that it is in fact a PVM for the standard basis. In fact pureState_projection' shows it's a projection whenever the vectors have length 1.

Equations

• POVM_PMF hUT hPS = PMF.ofFintype (fun (i : Fin k) => ↑⟨RCLike.re (pureState_C (e i) * ρ).trace, ⋯⟩) ⋯

def POVM_PMF_alt {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : 0 ≤ ρ) : PMF (Fin k)

Equations

• POVM_PMF_alt hUT hPS = PMF_of_preQuantumInstrument ⋯ hUT hPS

theorem POVM_PMF_eq_POVM_PMF_alt {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : 0 ≤ ρ) : POVM_PMF hUT hPS = POVM_PMF_alt hUT hPS

(pre)quantum instruments can be used as an alternative construction of our PMF.

def p {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hPS : 0 ≤ ρ) (i : Fin (k + 1)) : ENNReal

Probability measure with "lost" trace in the last outcome.

Equations

• p hPS i = if H : i = Fin.last k then some (1 - RCLike.re ρ.trace).toNNReal else let i_1 := i.castPred H; ↑⟨RCLike.re (pureState_C (e i_1) * ρ).trace, ⋯⟩

theorem p.ne_top {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hPS : 0 ≤ ρ) : ∑ a : Fin (k + 1), p hPS a ≠ ⊤

theorem trace_arithmetic {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : 0 ≤ ρ) : 1 = ↑(1 - RCLike.re ρ.trace).toNNReal + ↑(RCLike.re ρ.trace).toNNReal

def POVM_PMF_withTop₀ {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : 0 ≤ ρ) : PMF (Fin (k + 1))

May 8, 2026. Used to construct POVM_PMF_withTop.

Equations

• POVM_PMF_withTop₀ hUT hPS = PMF.ofFintype (p hPS) ⋯

noncomputable def POVM_PMF_withTop {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : 0 ≤ ρ) : PMF (Option (Fin k))

A PMF where the probability of none is the probability lost due to trace decrease.

Equations

• POVM_PMF_withTop hUT hPS = PMF.map (fun (i : Fin (k + 1)) => if x : i = Fin.last k then none else some (i.castPred x)) (POVM_PMF_withTop₀ hUT hPS)

theorem POVM_PMF_withTop_none {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : 0 ≤ ρ) : (POVM_PMF_withTop hUT hPS) none = ↑(RCLike.re (1 - ρ.trace)).toNNReal

POVM_PMF_withTop API, part 1: The lost probability is 1 - the trace.

theorem POVM_PMF_withTop_none₀ {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : 0 ≤ ρ) : (POVM_PMF_withTop ⋯ hPS) none = 0

POVM_PMF_withTop API, part 2: If the trace is one then no probability is lost.

theorem POVM_PMF_withTop_none₁ {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 0) (hPS : 0 ≤ ρ) : (POVM_PMF_withTop ⋯ hPS) none = 1

POVM_PMF_withTop API, part 3. If the trace is zero then all probability is lost.

noncomputable def POVM_subPMF {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : 0 ≤ ρ) : subPMF (Fin k)

Feb 1, 2026. An analogous construction from May 8, 2026 uses PMF (Fin (k+1)).

Equations

• POVM_subPMF hUT hPS = subPMF.ofFintype (Fin k) (fun (i : Fin k) => ↑⟨RCLike.re (pureState_C (e i) * ρ).trace, ⋯⟩) ⋯

def POVM_PMF' {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PMF (Fin k)

Equations

• POVM_PMF' hUT hPS = POVM_PMF hUT ⋯

noncomputable def POVM_subPMF' {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : ρ.PosSemidef) : subPMF (Fin k)

Equations

• POVM_subPMF' hUT hPS = POVM_subPMF hUT ⋯

theorem PMF₂₃help {R : Type u_1} [RCLike R] {ρ : Matrix (Fin 3) (Fin 3) R} (hPS : ρ.PosSemidef) : 0 ≤ ((pureState_C (e 0) + pureState_C (e 1)) * ρ).trace

theorem RCLike.re_sum {R : Type u_1} [RCLike R] {α : Type u_2} (s : Finset α) (f : α → R) : re (∑ i ∈ s, f i) = ∑ i ∈ s, re (f i)

Had to make this lemma as it seems missing in Mathlib.

theorem RCLike.sub_re {R : Type u_1} [RCLike R] (z w : R) : re (z - w) = re z - re w

Had to make this lemma as it seems missing in Mathlib.

theorem Finset.sum_erase_sub {k : ℕ} (c : Fin k) (J : Fin k → ℝ) : ∑ i : Fin k, J i - J c = ∑ i : Fin k with i ≠ c, J i

theorem PMF_of_state.sum_one_general {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : ∑ i : Fin 2, ↑(if i = 0 then ⟨RCLike.re ((1 - pureState_C (e acc)) * ρ).trace, ⋯⟩ else ⟨RCLike.re (pureState_C (e acc) * ρ).trace, ⋯⟩) = 1

theorem trace_nonneg_re {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hPS : ρ.PosSemidef) : 0 ≤ RCLike.re ρ.trace

theorem PMF_of_state.sum_one_general_general {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hPS : ρ.PosSemidef) : ∑ i : Fin 2, ↑(if i = 0 then ⟨RCLike.re ((1 - pureState_C (e acc)) * ρ).trace, ⋯⟩ else ⟨RCLike.re (pureState_C (e acc) * ρ).trace, ⋯⟩) = ↑⟨RCLike.re ρ.trace, ⋯⟩

noncomputable def PMF_of_state_general {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PMF (Fin 2)

Equations

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

noncomputable def PMF_of_state_CPTNI {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : ρ.PosSemidef) : PMF (Option (Fin 2))

May 9, 2026

Equations

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

noncomputable def subPMF_of_state_general {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : ρ.PosSemidef) : subPMF (Fin 2)

To use conditional computability here we would need to know the state had positive trace.

Equations

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

noncomputable def PMF_of_state_bern {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : ρ.PosSemidef) : PMF Bool

Feb 1, 2026: nonincreasing trace operators and a PMF.

Equations

• PMF_of_state_bern acc hUT hPS = PMF.bernoulli ⟨RCLike.re (pureState_C (e acc) * ρ).trace, ⋯⟩ ⋯

structure PVM : Type

Projection-valued measure.

• k : ℕ
• ρ : Matrix (Fin self.k) (Fin self.k) ℝ
• hρ : self.ρ.PosSemidef
• t : ℕ
• op : Fin self.t → Matrix (Fin self.k) (Fin self.k) ℝ
• pf (i : Fin self.t) : IsStarProjection (self.op i)
• p : PMF (Fin self.t)
• pf' (i : Fin self.t) : self.p i = ↑⟨(self.op i * self.ρ).trace, ⋯⟩

structure PVMeas : Type

Projection-valued measure. In this version we allow non-probability measures.

• k : ℕ
• ρ : Matrix (Fin self.k) (Fin self.k) ℝ
• hρ : self.ρ.PosSemidef
• t : ℕ
• op : Fin self.t → Matrix (Fin self.k) (Fin self.k) ℝ
• pf (i : Fin self.t) : IsStarProjection (self.op i)
• p : MeasureTheory.Measure (Fin self.t)
• pf' (i : Fin self.t) : self.p {i} = ↑⟨(self.op i * self.ρ).trace, ⋯⟩

structure PVMeas_C {R : Type u_1} [RCLike R] : Type u_1

Projection-valued measure. In this version we allow non-probability measures.

• k : ℕ
• ρ : Matrix (Fin self.k) (Fin self.k) R
• hρ : self.ρ.PosSemidef
• t : ℕ
• op : Fin self.t → Matrix (Fin self.k) (Fin self.k) R
• pf (i : Fin self.t) : IsStarProjection (self.op i)
• p : MeasureTheory.Measure (Fin self.t)
• pf' (i : Fin self.t) : self.p {i} = ↑⟨RCLike.re (self.op i * self.ρ).trace, ⋯⟩

structure PVM_C {R : Type u_1} [RCLike R] : Type u_1

• k : ℕ
• ρ : Matrix (Fin self.k) (Fin self.k) R
• hρ : self.ρ.PosSemidef
• t : ℕ
• op : Fin self.t → Matrix (Fin self.k) (Fin self.k) R
• pf (i : Fin self.t) : IsStarProjection (self.op i)
• p : PMF (Fin self.t)
• pf' (i : Fin self.t) : self.p i = ↑⟨RCLike.re (self.op i * self.ρ).trace, ⋯⟩

structure PVM_CPTNI {R : Type u_1} [RCLike R] : Type u_1

May 9, 2026.

• k : ℕ
• ρ : Matrix (Fin self.k) (Fin self.k) R
• hρ : self.ρ.PosSemidef
• t : ℕ
• op : Fin self.t → Matrix (Fin self.k) (Fin self.k) R
• pf (i : Fin self.t) : IsStarProjection (self.op i)
• p : PMF (Option (Fin self.t))
• pf' (i : Fin self.t) : self.p (some i) = ↑⟨RCLike.re (self.op i * self.ρ).trace, ⋯⟩

theorem trace_real_of_projection_and_pos_semidef {R : Type u_1} [RCLike R] {k : ℕ} {ρ O : Matrix (Fin k) (Fin k) R} (g₀ : ρ.IsHermitian) (g₁ : O.IsHermitian) : (O * ρ).trace = star (O * ρ).trace

theorem im_zero_PVM {R : Type u_1} [RCLike R] (M : PVM_C) (i : Fin M.t) : RCLike.im (M.op i * M.ρ).trace = 0

The probability is given as a real part of a complex number. Fortunately, the imaginary part is zero.

noncomputable def myPVM_C {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM_C

Equations

• myPVM_C hUT hPS = { k := k, ρ := ρ, hρ := hPS, t := k, op := fun (i : Fin k) => pureState_C (e i), pf := ⋯, p := POVM_PMF' hUT hPS, pf' := ⋯ }

noncomputable def myPVMeas_C_trace_one {R : Type u_1} [RCLike R] {k : ℕ} {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVMeas_C

Equations

• myPVMeas_C_trace_one hUT hPS = { k := k, ρ := ρ, hρ := hPS, t := k, op := fun (i : Fin k) => pureState_C (e i), pf := ⋯, p := (POVM_PMF' hUT hPS).toMeasure, pf' := ⋯ }

noncomputable def PVM_of_state_C {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM_C

Equations

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

noncomputable def PVM_of_state_CPTNI {R : Type u_1} [RCLike R] {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) R} (hUT : ρ.trace ≤ 1) (hPS : ρ.PosSemidef) : PVM_CPTNI

May 9, 2026.

Equations

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

def languageAcceptedBy_C {R : Type u_1} [RCLike R] {α : Type u_2} {q r : ℕ} (acceptStateIndex : Fin q.succ) (𝓚 : α → Fin r → Matrix (Fin q.succ) (Fin q.succ) R) : Set ((n : ℕ) × (Fin n → α))

Equations

• languageAcceptedBy_C acceptStateIndex 𝓚 = {word : (n : ℕ) × (Fin n → α) | krausApplyWord word.snd 𝓚 (pureState_C (e 0)) = pureState_C (e acceptStateIndex)}

theorem basisState_trace_one_C {R : Type u_1} [RCLike R] {k : ℕ} {i : Fin k.succ} : (pureState_C (e i)).trace = 1

noncomputable def PVM_of_word_of_channel_C {R : Type u_1} [RCLike R] {α : Type u_2} {r k : ℕ} (acc : Fin k.succ) {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) R} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) (word : (n : ℕ) × (Fin n → α)) : PVM_C

Equations

• PVM_of_word_of_channel_C acc h𝓚 word = PVM_of_state_C acc ⋯ ⋯

def MOlanguageAcceptedBy_C {R : Type u_1} [RCLike R] {α : Type u_2} {r k : ℕ} (acc : Fin k.succ) {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) R} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) : Set ((n : ℕ) × (Fin n → α))

Equations

• MOlanguageAcceptedBy_C acc h𝓚 = {word : (n : ℕ) × (Fin n → α) | (PVM_of_word_of_channel_C acc h𝓚 word).p 1 > 1 / 2}

noncomputable def PVM_of_word_of_operation {R : Type u_1} [RCLike R] {α : Type u_2} {r k : ℕ} (acc : Fin k.succ) {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) R} (h𝓚 : ∀ (a : α), QuantumOperation (𝓚 a)) (word : (n : ℕ) × (Fin n → α)) : PVM_CPTNI

Equations

• PVM_of_word_of_operation acc h𝓚 word = PVM_of_state_CPTNI acc ⋯ ⋯

def MOlanguageAcceptedBy_CPTNI {R : Type u_1} [RCLike R] {α : Type u_2} {r k : ℕ} (acc : Fin k.succ) {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) R} (h𝓚 : ∀ (a : α), QuantumOperation (𝓚 a)) : Set ((n : ℕ) × (Fin n → α))

May 9, 2026. Language accepted by a family of quantum operations, as opposed to quantum channels.

Equations

• MOlanguageAcceptedBy_CPTNI acc h𝓚 = {word : (n : ℕ) × (Fin n → α) | (PVM_of_word_of_operation acc h𝓚 word).p (some 1) > 1 / 2}

def exampleLanguage₀ : Set ((n : ℕ) × (Fin n → Fin 1))

Equations

• exampleLanguage₀ = MOlanguageAcceptedBy_CPTNI 0 exampleLanguage₀._proof_1

theorem matrix_1x1_nonneg_iff (x : ℂ) : 0 ≤ !![x] ↔ 0 ≤ x

def exampleLanguage₁ : Set ((n : ℕ) × (Fin n → Fin 1))

The matrix !![1 / 2] has trace < 1, but we are able to use it to define a language:

Equations

• exampleLanguage₁ = MOlanguageAcceptedBy_CPTNI 0 exampleLanguage₁._proof_1

theorem exampleLanguage₁_length_one (word : Fin 1 → Fin 1) : ⟨1, word⟩ ∉ exampleLanguage₁

May 10, 2026. Even though there is only one state and it is accepting, because of the trace-loss the length-one word is not accepted :)

theorem MO_language_nonempty_C {α : Type u_1} {r k : ℕ} {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℂ} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) : MOlanguageAcceptedBy_C 0 h𝓚 ≠ ∅

If the start and accept states are the same then the empty string is accepted in the measure-once setting.