Measurements in a ⋆-algebra

The measurements of the analyses, stated in any ⋆-algebra rather than in a matrix algebra, so that the same statements hold in the players' algebras of a bipartite model (MIPRE/Foundations/BipartiteModel.lean).

• IsPVMIn P: a projective measurement, self-adjoint idempotents summing to one and mutually orthogonal. In a matrix algebra, or any C*-algebra, orthogonality follows from the other three (MIPRE.IsPVM.orthogonal for matrices); in a general ring it does not, so it is a field.
• POVMIn X R: a positive operator valued measure in an ordered ⋆-algebra, with the fields of the matrix MIPRE.POVM verbatim, so that a matrix POVM is one (MIPRE.POVM.toIn).
• pvmObs P ε = ∑_a ε a • P a, the observable of a weighting of the outcomes, a ring homomorphism in ε for a projective measurement (IsPVMIn.pvmObs_mul).

The matrix versions (MIPRE/Foundations/PVM.lean, MIPRE/Foundations/POVMValue.lean) are these in Matrix n n ℂ.

Projective measurements

structure MIPRE.IsPVMIn {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] (P : Λ → R) : Prop

A projective measurement in a ⋆-ring: self-adjoint idempotents, summing to one and mutually orthogonal.

• star_eq (a : Λ) : star (P a) = P a

  Each element is self-adjoint.

• idem (a : Λ) : P a * P a = P a

  Each element is idempotent.

• sum_eq_one : ∑ a : Λ, P a = 1

  The elements sum to one.

• orthogonal {a b : Λ} : a ≠ b → P a * P b = 0

  Distinct elements are orthogonal.

theorem MIPRE.IsPVMIn.isStarProjection {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) (a : Λ) : IsStarProjection (P a)

theorem MIPRE.IsPVMIn.nonneg {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} [PartialOrder R] [StarOrderedRing R] (h : IsPVMIn P) (a : Λ) : 0 ≤ P a

In a star-ordered ring, the elements of a projective measurement are nonnegative.

theorem MIPRE.IsPVMIn.mul_eq_ite {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} [DecidableEq Λ] (h : IsPVMIn P) (a b : Λ) : P a * P b = if a = b then P a else 0

P a * P b is P a on the diagonal and zero off it.

theorem MIPRE.IsPVMIn.coarse {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} {Λ' : Type u_3} [Fintype Λ'] [DecidableEq Λ'] (h : IsPVMIn P) (f : Λ → Λ') : IsPVMIn fun (c : Λ') => ∑ a : Λ with f a = c, P a

Coarse-graining a projective measurement gives a projective measurement.

theorem MIPRE.IsPVMIn.map {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} {S : Type u_3} {F : Type u_4} [Ring S] [StarRing S] [FunLike F R S] [RingHomClass F R S] [StarHomClass F R S] (f : F) (h : IsPVMIn P) : IsPVMIn fun (a : Λ) => f (P a)

The image of a projective measurement under a unital ⋆-ring homomorphism is one.

The marginals of a projective measurement with a product outcome set

theorem MIPRE.IsPVMIn.marg_mul_marg {R : Type u_1} [Ring R] [StarRing R] {B : Type u_3} {C : Type u_4} [Fintype B] [Fintype C] {Q : B × C → R} (h : IsPVMIn Q) (b : B) (c : C) : (∑ b' : B, Q (b', c)) * ∑ c' : C, Q (b, c') = Q (b, c)

The two marginals of a projective measurement multiply to the joint element: the off-diagonal terms of the product vanish by orthogonality, and the surviving one is idempotent.

theorem MIPRE.IsPVMIn.marg_mul_marg' {R : Type u_1} [Ring R] [StarRing R] {B : Type u_3} {C : Type u_4} [Fintype B] [Fintype C] {Q : B × C → R} (h : IsPVMIn Q) (b : B) (c : C) : (∑ c' : C, Q (b, c')) * ∑ b' : B, Q (b', c) = Q (b, c)

The other order.

theorem MIPRE.IsPVMIn.sum_marg_left {R : Type u_1} [Ring R] [StarRing R] {B : Type u_3} {C : Type u_4} [Fintype B] [Fintype C] {Q : B × C → R} (h : IsPVMIn Q) : ∑ b : B, ∑ c : C, Q (b, c) = 1

theorem MIPRE.IsPVMIn.sum_marg_right {R : Type u_1} [Ring R] [StarRing R] {B : Type u_3} {C : Type u_4} [Fintype B] [Fintype C] {Q : B × C → R} (h : IsPVMIn Q) : ∑ c : C, ∑ b : B, Q (b, c) = 1

theorem MIPRE.IsPVMIn.marg_left {R : Type u_1} [Ring R] [StarRing R] {B : Type u_3} {C : Type u_4} [Fintype B] [Fintype C] {Q : B × C → R} (h : IsPVMIn Q) : IsPVMIn fun (b : B) => ∑ c : C, Q (b, c)

The marginal forgetting the second outcome is projective.

theorem MIPRE.IsPVMIn.marg_right {R : Type u_1} [Ring R] [StarRing R] {B : Type u_3} {C : Type u_4} [Fintype B] [Fintype C] {Q : B × C → R} (h : IsPVMIn Q) : IsPVMIn fun (c : C) => ∑ b : B, Q (b, c)

The marginal forgetting the first outcome is projective.

The observable of a weighting

def MIPRE.pvmObs {R : Type u_1} {Λ : Type u_2} [Fintype Λ] [AddCommMonoid R] [Module ℂ R] (P : Λ → R) (ε : Λ → ℂ) : R

∑_a ε a • P a, the operator a weighting of a measurement's outcomes defines.

Equations

• MIPRE.pvmObs P ε = ∑ a : Λ, ε a • P a

theorem MIPRE.IsPVMIn.pvmObs_mul {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) (ε δ : Λ → ℂ) : pvmObs P ε * pvmObs P δ = pvmObs P (ε * δ)

pvmObs P is multiplicative for a projective measurement.

theorem MIPRE.IsPVMIn.pvmObs_const {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) (c : ℂ) : (pvmObs P fun (x : Λ) => c) = c • 1

theorem MIPRE.IsPVMIn.pvmObs_one {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) : pvmObs P 1 = 1

theorem MIPRE.IsPVMIn.star_pvmObs {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} [StarModule ℂ R] (h : IsPVMIn P) (ε : Λ → ℂ) : star (pvmObs P ε) = pvmObs P (star ε)

theorem MIPRE.IsPVMIn.pvmObs_star_eq {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} [StarModule ℂ R] (h : IsPVMIn P) {ε : Λ → ℂ} (hε : ∀ (a : Λ), star (ε a) = ε a) : star (pvmObs P ε) = pvmObs P ε

A real weighting gives a self-adjoint operator.

theorem MIPRE.IsPVMIn.pvmObs_mul_self {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) {ε : Λ → ℂ} (hε : ∀ (a : Λ), ε a * ε a = 1) : pvmObs P ε * pvmObs P ε = 1

A weighting squaring to one pointwise gives an operator squaring to one.

theorem MIPRE.IsPVMIn.pvmObs_comm {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) (ε δ : Λ → ℂ) : pvmObs P ε * pvmObs P δ = pvmObs P δ * pvmObs P ε

Two weightings of the same measurement commute.

theorem MIPRE.IsPVMIn.pvmObs_mul_mul {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Fintype Λ] {P : Λ → R} (h : IsPVMIn P) {ε δ η : Λ → ℂ} {s : ℂ} (hs : ∀ (a : Λ), ε a * δ a * η a = s) : pvmObs P ε * pvmObs P δ * pvmObs P η = s • 1

Three weightings whose pointwise product is the constant s multiply to s • 1 exactly.

Positive operator valued measures

structure MIPRE.POVMIn (X : Type u_3) (R : Type u_4) [Fintype X] [Ring R] [StarRing R] [PartialOrder R] : Type (max u_3 u_4)

A positive operator valued measure in an ordered ⋆-ring, with outcomes X: the fields of the matrix MIPRE.POVM.

• mats : X → ↥(selfAdjoint R)

  The measurement operators, one for each outcome.

• nonneg (x : X) : 0 ≤ self.mats x

  Each measurement operator is nonnegative.

• normalized : ∑ x : X, self.mats x = 1

  The measurement operators sum to one.

def MIPRE.POVMIn.op {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] (M : POVMIn X R) (x : X) : R

The measurement operator of an outcome, as an element of R.

Equations

• M.op x = ↑(M.mats x)

theorem MIPRE.POVMIn.ext' {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] {M N : POVMIn X R} (h : ∀ (x : X), M.op x = N.op x) : M = N

A POVM is determined by its operators; the other fields are propositions.

theorem MIPRE.POVMIn.star_op {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] (M : POVMIn X R) (x : X) : star (M.op x) = M.op x

theorem MIPRE.POVMIn.sum_op {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] (M : POVMIn X R) : ∑ x : X, M.op x = 1

theorem MIPRE.POVMIn.op_nonneg {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] (M : POVMIn X R) (x : X) : 0 ≤ M.op x

theorem MIPRE.POVMIn.op_le_one {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn X R) (x : X) : M.op x ≤ 1

Each measurement operator is at most one.

def MIPRE.POVMIn.map {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Y : Type u_4} [Fintype Y] [DecidableEq Y] (f : X → Y) (M : POVMIn X R) : POVMIn Y R

The coarse-graining of a POVM along a map of outcomes: each new outcome gets the sum of the operators of its fibre.

Equations

• MIPRE.POVMIn.map f M = { mats := fun (y : Y) => ∑ x : X with f x = y, M.mats x, nonneg := ⋯, normalized := ⋯ }

theorem MIPRE.POVMIn.map_op {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Y : Type u_4} [Fintype Y] [DecidableEq Y] (f : X → Y) (M : POVMIn X R) (y : Y) : (map f M).op y = ∑ x : X with f x = y, M.op x

theorem MIPRE.POVMIn.sum_op_map_prod {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {B : Type u_4} {C : Type u_5} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (M : POVMIn X R) (f : X → B) (g : X → C) (b : B) : ∑ c : C, (map (fun (a : X) => (f a, g a)) M).op (b, c) = (map f M).op b

The marginal of a jointly coarse-grained POVM is the coarse-graining of one component: the fibres of (f, g) over {b} × C partition the fibre of f over b.

theorem MIPRE.POVMIn.sum_op_map_prod' {R : Type u_1} {X : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {B : Type u_4} {C : Type u_5} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (M : POVMIn X R) (f : X → B) (g : X → C) (c : C) : ∑ b : B, (map (fun (a : X) => (f a, g a)) M).op (b, c) = (map g M).op c

The other marginal.