PhyslibAlpha.AlgebraicFramework.OrderUnit.Channel.MeasureAndPrepare

Measure-and-prepare channels

i. Overview

A channel `E₂ →ₚ₁[ℝ] E₁` (the Heisenberg picture of a Schrödinger channel `E₁ → E₂`) is measure-and-prepare when it factors through a finite classical system: measure the input, then prepare a (possibly different) output state for each outcome. Dually, this is exactly `Φ = M.comp P` for a measurement `M : (ι → ℝ) →ₚ₁[ℝ] E₁` (`Measurement/ClassicalSystem.lean`) and a "preparation" `P : E₂ →ₚ₁[ℝ] (ι → ℝ)` — itself a channel into the classical system, so a family of states on `E₂` indexed by `ι`, bundled the same way `Measurement` bundles a family of effects.

This is the abstract, order-unit-level version of an entanglement-breaking channel: the factorization definition extends to any outcome type (not just finite ones) with no change, unlike a hard-coded sum over a fixed outcome set.

ii. Key definitions

`UnitalPositiveLinearMap.IsMeasureAndPrepare`

iii. Table of contents

A. Factorization through a finite classical system

A. Factorization through a finite classical system

1 declaration

definition

Measure-and-prepare property of a channel $\Phi$

#IsMeasureAndPrepare

A unital positive linear map $\Phi : E_2 \to E_1$ is said to be **measure-and-prepare** if it factors through a finite classical system. Specifically, $\Phi$ satisfies this property if there exists a finite set of outcomes $\iota$ , a measurement channel $M : (\iota \to \mathbb{R}) \to E_1$ , and a preparation channel $P : E_2 \to (\iota \to \mathbb{R})$ such that $\Phi = M \circ P$ . Here, the notation $\to_{p1}$ denotes unital positive linear maps, which represent channels in the Heisenberg picture.