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:

• J. Lakshmanan, 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, preprint 2026.

• Li, Lvzhou and Qiu, Daowen and Zou, Xiangfu and Li, Lvjun and Wu, Lihua and Mateus, Paulo, Characterizations of one-way general quantum finite automata, 2012

• Yakary{\i}lmaz, Abuzer and Say, A. C. Cem, Unbounded-error quantum computation with small space bounds, 2011

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_psd {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {q r : ℕ} (K : Fin r → Matrix (Fin q) (Fin q) R) (ρ : Matrix (Fin q) (Fin 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 r : ℕ} (K : Fin r → Matrix (Fin q) (Fin q) R) : Prop

Equations

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

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

Equations

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

def densityMatrix {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] (q : ℕ) : Type u_1

Equations

• densityMatrix q = { ρ : Matrix (Fin q) (Fin q) R // ρ.PosSemidef ∧ ρ.trace = 1 }

def subNormalizedDensityMatrix {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] (q : ℕ) : Type u_1

Equations

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

def quantum_channel {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] (q r : ℕ) : Type u_1

Equations

• quantum_channel q r = { K : Fin r → Matrix (Fin q) (Fin q) R // ∑ i : Fin r, (K i).conjTranspose * K i = 1 }

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

instance instPartialOrderOfRCLike_kraus {R : Type u_1} [RCLike R] : PartialOrder R

Equations

• instPartialOrderOfRCLike_kraus = RCLike.toPartialOrder

theorem quantum_channel_preserves_trace {R : Type u_1} [CommRing R] [PartialOrder R] [StarRing R] {q r : ℕ} (K : quantum_channel q r) (ρ : Matrix (Fin q) (Fin q) R) : (krausApply (↑K) ρ).trace = ρ.trace

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

def krausApply_densityMatrix {R : Type u_1} [CommRing R] [PartialOrder R] [StarRing R] [AddLeftMono R] {q r : ℕ} (K : Fin r → Matrix (Fin q) (Fin q) R) (hq : quantumChannel K) (ρ : densityMatrix q) : densityMatrix q

Realizing a quantumChannel as a map on densityMatrices.

Equations

• krausApply_densityMatrix K hq ρ = ⟨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} (hq : ∀ (a : α), quantumChannel (𝓚 a)) (ρ : densityMatrix q) : (krausApplyWord word 𝓚 ↑ρ).PosSemidef ∧ (krausApplyWord word 𝓚 ↑ρ).trace = 1

As long as we have a quantum channel, 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 q) : densityMatrix q

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

Equations

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

def krausApplyWord_channel {α : Type u_1} {R : Type u_2} [CommRing R] [StarRing R] [PartialOrder R] [AddLeftMono R] {n q r : ℕ} (word : Fin n → α) (𝓚 : α → quantum_channel q r) (ρ : densityMatrix q) : densityMatrix q

Equations

• krausApplyWord_channel word 𝓚 ρ = krausApplyWord_map word (fun (a : α) => ↑(𝓚 a)) ⋯ ρ

def grudka_Z : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) ℤ

The example Kraus operators from QCNC submission.

Equations

• grudka_Z = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![0, -1, 0; 1, 0, 0; 0, 0, 1], 0]]

def grudka_R₀ {R : Type u_1} [RCLike R] : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) R

Equations

• grudka_R₀ = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![0, -1, 0; 1, 0, 0; 0, 0, 1], 0]]

noncomputable def grudka_R (θ : ℝ) : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) ℝ

Equations

• grudka_R θ = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![Real.cos θ, -Real.sin θ, 0; Real.sin θ, Real.cos θ, 0; 0, 0, 1], 0]]

noncomputable def grudka_C (θ : ℂ) : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) ℂ

Equations

• grudka_C θ = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![Complex.cos θ, -Complex.sin θ, 0; Complex.sin θ, Complex.cos θ, 0; 0, 0, 1], 0]]

theorem grudka_B_quantumChannel (θ : ℝ) : quantumChannel (grudka_R θ 1)

1/24/26

theorem grudka_A_quantumChannel (θ : ℝ) : quantumChannel (grudka_R θ 0)

theorem grudka_quantumChannel (θ : ℝ) (i : Fin 2) : quantumChannel (grudka_R θ i)

noncomputable def grudka_map (θ : ℝ) {n : ℕ} (word : Fin n → Fin 2) : densityMatrix 3 → densityMatrix 3

Grudka et al.' map does indeed map density matrices to density matrices.

Equations

• grudka_map θ word = krausApplyWord_map word (grudka_R θ) ⋯

def e₁ {R : Type u_1} [One R] [Zero R] : Matrix (Fin 3) (Fin 1) R

Equations

• e₁ = ![1, 0, 0]

def e₂ {R : Type u_1} [One R] [Zero R] : Matrix (Fin 3) (Fin 1) R

Equations

• e₂ = ![0, 1, 0]

def e₃ {R : Type u_1} [One R] [Zero R] : Matrix (Fin 3) (Fin 1) R

Equations

• e₃ = ![0, 0, 1]

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

Equations

• e i = Matrix.single i 0 1

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

Equations

• pureState e = e.mulᵣ e.transpose

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

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

theorem pureState_selfAdjoint {k : ℕ} (e : Matrix (Fin k) (Fin 1) ℝ) : (pureState 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

• ⋯ = ⋯

def pureState_projection' {k : ℕ} (e : EuclideanSpace ℝ (Fin k)) (he : ‖e‖ = 1) : IsStarProjection (pureState fun (i : Fin k) (x : Fin 1) => e.ofLp i)

Equations

• ⋯ = ⋯

theorem pureState_projection {k : ℕ} (i : Fin k) : IsStarProjection (pureState (e i))

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

theorem pureState_projection'' : IsStarProjection (pureState (e 0) + pureState (e 1))

Projection onto span ⟨e₁, e₂⟩ is indeed a star-projection. So we could form a PMF with two outcomes (e₁,e₂) vs. e₃.

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) (this : 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 →₀ ℝ) (this : 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 pureState_psd {k : ℕ} (e : Matrix (Fin k) (Fin 1) ℝ) : (e.mulᵣ e.transpose).PosSemidef

theorem matrix_identity_general {R : Type u_1} [RCLike R] (k : ℕ) (e : Matrix (Fin k) (Fin 1) R) (α : Fin k → R) : star α ⬝ᵥ (e * e.conjTranspose).mulVec α = (Matrix.vecMul (star α) e * e.conjTranspose.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 pureState_probability_one {ρ : Matrix (Fin 3) (Fin 3) ℝ} (hρ : ρ.trace = 1) : (pureState e₁ * ρ).trace + (pureState e₂ * ρ).trace + (pureState e₃ * ρ).trace = 1

The positive operator pureState e₁ is chosen with probability (pureState e₁ * ρ).trace.

theorem pureState_probability_one_C {R : Type u_1} [RCLike R] {ρ : Matrix (Fin 3) (Fin 3) R} (hρ : ρ.trace = 1) : (pureState_C e₁ * ρ).trace + (pureState_C e₂ * ρ).trace + (pureState_C e₃ * ρ).trace = 1

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

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

Equations

• instNormedRingMatrixFinOfNatNatComplex_kraus = Matrix.frobeniusNormedRing

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

Equations

• instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus = Matrix.frobeniusNormedAlgebra

theorem matrix_posSemidef_eq_star_mul_self' {n : ℕ} (P : Matrix (Fin n) (Fin n) ℝ) (hP : 0 ≤ P) : ∃ (B : Matrix (Fin n) (Fin n) ℝ), P = star B * B

Jireh recommends this approach.

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

instance instPartialOrderOfRCLike_kraus_1 {R : Type u_1} [RCLike R] : PartialOrder R

Equations

• instPartialOrderOfRCLike_kraus_1 = RCLike.toPartialOrder

instance instStarOrderedRing_kraus {R : Type u_1} [RCLike R] : StarOrderedRing R

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_reduces_trace {R : Type u_1} [RCLike R] {q r : ℕ} (K : Fin r → Matrix (Fin q) (Fin q) R) (hq : quantumOperation K) (ρ : Matrix (Fin q) (Fin q) R) (hρ : 0 ≤ ρ) : (krausApply K ρ).trace ≤ ρ.trace

Feb 1, 2026

theorem quantumOperation_preserves_trace_le_one {R : Type u_1} [RCLike R] {q r : ℕ} (K : Fin r → Matrix (Fin q) (Fin q) R) (hq : 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) (hq : quantumOperation K) (ρ : subNormalizedDensityMatrix q) : subNormalizedDensityMatrix q

Feb 1, 2026 Realizing a quantumChannel as a map on densityMatrices.

Equations

• krausApply_subNormalizedDensityMatrix K hq ρ = ⟨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} (hq : ∀ (a : α), quantumOperation (𝓚 a)) (ρ : subNormalizedDensityMatrix 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) (hq : ∀ (a : α), quantumOperation (𝓚 a)) (ρ : subNormalizedDensityMatrix q) : subNormalizedDensityMatrix q

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

Equations

• krausApplyWord_map_sub word 𝓚 hq ρ = ⟨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' {n : ℕ} {ρ : Matrix (Fin n) (Fin n) ℝ} (hρ' : ρ.PosSemidef) (e : Matrix (Fin n) (Fin 1) ℝ) (he : ‖WithLp.toLp 2 fun (i : Fin n) => e i 0‖ = 1) : 0 ≤ (pureState e * ρ).trace

A general reason why nonneg_trace below holds. Can be generalized to let (e * eᵀ) be any projection, see above ^^.

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 {n : ℕ} {ρ : Matrix (Fin n) (Fin n) ℝ} (hρ' : ρ.PosSemidef) (i : Fin n) : 0 ≤ (pureState (e i) * ρ).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 {k : ℕ} (ρ : Matrix (Fin k) (Fin k) ℝ) : ∑ x : Fin k, Matrix.of (Function.update 0 x (ρ.row x)) = ρ

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 POVM_PMF.aux₀ {k : ℕ} {ρ : Matrix (Fin k) (Fin k) ℝ} (hρ : ρ.trace = 1) (hρ' : ρ.PosSemidef) : ∑ a : Fin k, ⟨(pureState (e a) * ρ).trace, ⋯⟩ = ENNReal.toNNReal 1

theorem standard_basis_probability_one {k : ℕ} {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : ∑ a : Fin k, ↑⟨(pureState (e a) * ρ).trace, ⋯⟩ = 1

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_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 ⋯

noncomputable 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, ⋯⟩) ⋯

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

Equations

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

noncomputable 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

def PVM_PMF₂₃ {ρ : Matrix (Fin 3) (Fin 3) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PMF (Fin 2)

A probability measure that gives the probability of being in the xy-plane, or the z-axis, for a given PSD trace-one matrix ρ. See myPVM₂₃ below.

Equations

• PVM_PMF₂₃ hUT hPS = PMF.ofFintype (fun (i : Fin 2) => ↑(if i = 0 then ⟨((pureState (e 0) + pureState (e 1)) * ρ).trace, ⋯⟩ else ⟨(pureState (e 2) * ρ).trace, ⋯⟩)) ⋯

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

theorem one_eq_sum_pureState_R {k : ℕ} : 1 = ∑ i : Fin k, pureState (e i)

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 trace_one_sub {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hPS : ρ.PosSemidef) : 0 ≤ ((1 - pureState (e acc)) * ρ).trace

theorem PMF_of_state.sum_one {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : ∑ i : Fin 2, ↑(if i = 0 then ⟨((1 - pureState (e acc)) * ρ).trace, ⋯⟩ else ⟨(pureState (e acc) * ρ).trace, ⋯⟩) = 1

theorem ofReal_inj_aux {k : ℕ} (J : Fin k → ℝ) (hnn : ∀ (a : Fin k), J a ≥ 0) : ∑ a : Fin k, ⟨J a, ⋯⟩ = ⟨∑ a : Fin k, J a, ⋯⟩

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 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 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

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, ⋯⟩

def PMF_of_state {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PMF (Fin 2)

Defining a Bernoulli probability measure by declaring that e_{acc} is the accepted subspace.

Equations

• PMF_of_state acc hUT hPS = PMF.ofFintype (fun (i : Fin 2) => ↑(if i = 0 then ⟨((1 - pureState (e acc)) * ρ).trace, ⋯⟩ else ⟨(pureState (e acc) * ρ).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 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 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, ⋯⟩

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 {k : ℕ} {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM

Equations

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

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' := ⋯ }

def myPVM₂₃ {ρ : Matrix (Fin 3) (Fin 3) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM

Equations

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

def PVM_of_state {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM

Equations

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

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.

def languageAcceptedBy {α : Type u_1} {q r : ℕ} (acceptStateIndex : Fin q.succ) (𝓚 : α → Fin r → Matrix (Fin q.succ) (Fin q.succ) ℝ) : Set ((n : ℕ) × (Fin n → α))

1/24/26

Equations

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

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 grudka_helper : Matrix.mulᵣ ![1, 0, 0] (Matrix.transpose ![1, 0, 0]) = !![1, 0, 0; 0, 0, 0; 0, 0, 0]

theorem basisState_trace_one {k : ℕ} {i : Fin k.succ} : (pureState (e i)).trace = 1

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

def PVM_of_word_of_channel {α : Type u_1} {r k : ℕ} (acc : Fin k.succ) (𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℝ) (h𝓚 : ∀ (a : α), quantumChannel (𝓚 a)) (word : (n : ℕ) × (Fin n → α)) : PVM

The projection-valued measure corresponding to word belong to the measure-once language of KOA 𝓚.

Equations

• PVM_of_word_of_channel acc 𝓚 h𝓚 word = PVM_of_state acc ⋯ ⋯

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 getPVM₃ {α : Type u_1} {r : ℕ} (𝓚 : α → Fin r → Matrix (Fin (Nat.succ 2)) (Fin (Nat.succ 2)) ℝ) (h𝓚 : ∀ (a : α), quantumChannel (𝓚 a)) (word : (n : ℕ) × (Fin n → α)) : PVM

Equations

• getPVM₃ 𝓚 h𝓚 word = PVM_of_word_of_channel 2 𝓚 h𝓚 word

def MOlanguageAcceptedBy {α : Type u_1} {r k : ℕ} (acc : Fin k.succ) (𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℝ) (h𝓚 : ∀ (a : α), quantumChannel (𝓚 a)) : Set ((n : ℕ) × (Fin n → α))

1/25/26 We accept word if starting in e₀ we end up in e₁ with probability at least 1/2.

Equations

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

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 (id 1) > 1 / 2}

theorem MO_language_nonempty {α : Type u_1} {r k : ℕ} (𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℝ) (h𝓚 : ∀ (a : α), quantumChannel (𝓚 a)) : MOlanguageAcceptedBy 0 𝓚 h𝓚 ≠ ∅

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

theorem MO_grudka0_language_nonempty : MOlanguageAcceptedBy 0 (grudka_R 0) ⋯ ≠ ∅

For the Grudka channel with start state 0, the probability of accepting the empty word is 1 > 1/2 hence ![] is in the corresponding measure-once language. This can be generalized to any quantum channel.

def MOlanguageAcceptedBy₃ {α : Type u_1} {r : ℕ} (𝓚 : α → Fin r → Matrix (Fin 3) (Fin 3) ℝ) (h𝓚 : ∀ (a : α), quantumChannel (𝓚 a)) : Set ((n : ℕ) × (Fin n → α))

Measure-Once language accepted by 𝓚 is {word | Probability that we are in state e₃, and not in the span of e₁,e₂, > 1/2}. q = 2 because we haven't generalized myPVM₂₃ yet

Equations

• MOlanguageAcceptedBy₃ 𝓚 h𝓚 = MOlanguageAcceptedBy 1 𝓚 h𝓚

def MOlanguageAcceptedBy' {α : Type u_1} {r : ℕ} (𝓚 : α → quantum_channel 3 r) : Set ((n : ℕ) × (Fin n → α))

Equations

• MOlanguageAcceptedBy' 𝓚 = {word : (n : ℕ) × (Fin n → α) | (getPVM₃ (fun (a : α) => ↑(𝓚 a)) ⋯ word).p (id 1) > 1 / 2}

theorem grudka_language_nonempty : languageAcceptedBy 0 (grudka_R 0) ≠ ∅

theorem grudka₀_basic_operation : krausApply (grudka_R₀ 0) (pureState e₁) = pureState e₂

theorem grudka_basic_operation : krausApply (grudka_R 0 0) (pureState e₁) = pureState e₂

theorem grudka_basic_operation₂ : krausApply (grudka_R₀ 0) (pureState e₂) = pureState e₃

theorem MO_grudka1_language_nonempty : MOlanguageAcceptedBy 1 (grudka_R 0) ⋯ ≠ ∅