Matrix-valued measurements for the MIP*=RE project

This file provides the matrix-valued measurement layer used by the LDT formalization.

Main definitions

• Submeasurement — a family of PSD matrices summing to at most the identity.
• Measurement — a family of PSD matrices summing to exactly the identity.
• Submeasurement.postprocess — data-processed submeasurements via answer relabeling.
• Measurement.postprocess — the paper's postprocessing proposition for complete POVMs.
• inconsistency — the off-diagonal mass ∑_{a ≠ b} τ(M_a N_b).
• diagOverlap — the diagonal mass ∑_a τ(M_a N_a).

References

This file builds the project's finite-dimensional measurement layer on top of the normalized-trace and positive-operator facts in MIPStarRE.Quantum.FiniteMatrix for the quantum formalization in references/ldt-paper/.

Submeasurements and measurements

structure MIPStarRE.Quantum.Submeasurement (α : Type u_1) [Fintype α] (d : Type u_2) [Fintype d] [DecidableEq d] : Type (max u_1 u_2)

A submeasurement on a finite answer type α is a family of PSD matrices M : α → Op d with ∑ a, M a ≤ 1.

• effect : α → Op d

  The effect operators.

• pos (a : α) : 0 ≤ self.effect a

  Each effect is positive semidefinite.

• sum_le_one : ∑ a : α, self.effect a ≤ 1

  The effects sum to at most the identity.

structure MIPStarRE.Quantum.Measurement (α : Type u_1) [Fintype α] (d : Type u_2) [Fintype d] [DecidableEq d] extends MIPStarRE.Quantum.Submeasurement α d : Type (max u_1 u_2)

A measurement is a submeasurement whose effects sum exactly to the identity.

• effect : α → Op d
• pos (a : α) : 0 ≤ self.effect a
• sum_le_one : ∑ a : α, self.effect a ≤ 1
• sum_eq_one : ∑ a : α, self.effect a = 1

  The effects sum to the identity.

Totals and postprocessing

Totals and postprocessing

noncomputable def MIPStarRE.Quantum.Submeasurement.total {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} [Fintype α] (M : Submeasurement α d) : Op d

The total operator ∑ a, M_a.

Equations

• M.total = ∑ a : α, M.effect a

noncomputable def MIPStarRE.Quantum.Submeasurement.postprocess {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Submeasurement α d) (f : α → β) : Submeasurement β d

Data processing: relabel the answer set by f : α → β, summing the effects over fibers.

Equations

• M.postprocess f = { effect := fun (b : β) => ∑ a : α with f a = b, M.effect a, pos := ⋯, sum_le_one := ⋯ }

theorem MIPStarRE.Quantum.Submeasurement.total_le_one {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} [Fintype α] (M : Submeasurement α d) : M.total ≤ 1

Restatement of sum_le_one in terms of the named total operator.

theorem MIPStarRE.Quantum.Submeasurement.postprocess_sum_eq {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Submeasurement α d) (f : α → β) : ∑ a : α, M.effect a = ∑ b : β, (M.postprocess f).effect b

Postprocessing preserves the sum of all effects.

theorem MIPStarRE.Quantum.Submeasurement.postprocess_total {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Submeasurement α d) (f : α → β) : (M.postprocess f).total = M.total

Postprocessing preserves the named total operator.

def MIPStarRE.Quantum.Measurement.ofSumEqOne {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} [Fintype α] (effect : α → Op d) (pos : ∀ (a : α), 0 ≤ effect a) (sum_eq_one : ∑ a : α, effect a = 1) : Measurement α d

Build a complete measurement from effects whose sum is exactly the identity.

This constructor keeps the equality proof as the primary hypothesis and derives the inherited submeasurement inequality automatically. It is useful at paper sites that are explicitly POVMs rather than relaxed sub-POVMs.

Equations

• MIPStarRE.Quantum.Measurement.ofSumEqOne effect pos sum_eq_one = { effect := effect, pos := pos, sum_le_one := ⋯, sum_eq_one := sum_eq_one }

theorem MIPStarRE.Quantum.Measurement.total_eq_one {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} [Fintype α] (M : Measurement α d) : M.total = 1

The named total of a complete measurement is the identity.

noncomputable def MIPStarRE.Quantum.Measurement.postprocess {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Measurement α d) (f : α → β) : Measurement β d

Postprocess a complete measurement by relabeling outcomes.

This formalizes references/ldt-paper/preliminaries.tex:169--180: regrouping the effects along the fibers of f preserves the total operator, so a POVM remains a POVM after postprocessing.

Equations

• M.postprocess f = { toSubmeasurement := M.postprocess f, sum_eq_one := ⋯ }

@[simp]

theorem MIPStarRE.Quantum.Measurement.postprocess_effect {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Measurement α d) (f : α → β) (b : β) : (M.postprocess f).effect b = ∑ a : α with f a = b, M.effect a

@[simp]

theorem MIPStarRE.Quantum.Measurement.postprocess_to_submeasurement {d : Type u_1} [Fintype d] [DecidableEq d] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Measurement α d) (f : α → β) : (M.postprocess f).toSubmeasurement = M.postprocess f

Overlap definitions

noncomputable def MIPStarRE.Quantum.inconsistency {d : Type u_1} [Fintype d] {α : Type u_2} [Fintype α] [DecidableEq α] (M N : α → Op d) : ℂ

The off-diagonal overlap mass ∑_{a ≠ b} τ(M_a N_b).

Equations

• MIPStarRE.Quantum.inconsistency M N = ∑ a : α, ∑ b : α with b ≠ a, MIPStarRE.Quantum.normalizedTrace (M a * N b)

noncomputable def MIPStarRE.Quantum.diagOverlap {d : Type u_1} [Fintype d] {α : Type u_2} [Fintype α] (M N : α → Op d) : ℂ

The diagonal overlap mass ∑_a τ(M_a N_a).

Equations

• MIPStarRE.Quantum.diagOverlap M N = ∑ a : α, MIPStarRE.Quantum.normalizedTrace (M a * N a)