Core submeasurement structures for the low individual degree test

Foundational measurement, submeasurement, and projective-measurement structures: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/SubMeasurementCore.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The vendored structures have their effects in the matrix algebra Op ι. Here they are generic over an ordered ⋆-ring R ([Ring R] [StarRing R] [PartialOrder R]), with the vendored field names verbatim: local families take R = 𝔓, the local C*-algebra of a symmetric model, and joint families R = K →L[ℂ] K. Each lemma asks for what its proof uses: positivity facts for a star-ordered ring, and the two projective lemmas (ProjSubMeas.outcome_mul_total_eq_outcome, ProjSubMeas.outcome_orthogonal) for a C*-algebra, where the C*-identity star x * x = 0 → x = 0 (CStarRing.star_mul_self_eq_zero_iff) replaces the vendored Matrix.conjTranspose_mul_self_eq_zero.

New here

• SubMeas.map, Measurement.map, ProjSubMeas.map, ProjMeas.map: the image of a (sub)measurement under a ⋆-algebra homomorphism. This is how the port places a local family on a tensor factor: the vendored SubMeas.liftLeft (LDT/Basic/SubMeasurementFamilies.lean) becomes A.map S.L, and liftRight becomes A.map S.R.
• The bridges to the repository's measurement vocabulary (MIPRE/Foundations/Measurement.lean): Measurement.toPOVMIn and Measurement.ofPOVMIn, inverse to each other, and ProjMeas.isPVMIn and ProjMeas.ofIsPVMIn.

Not ported

Every declaration of the vendored file has a counterpart here.

structure MIPRE.LIDT.Co.SubMeas (α : Type u_1) [Fintype α] (R : Type u_2) [Ring R] [StarRing R] [PartialOrder R] : Type (max u_1 u_2)

A paper-local submeasurement with outcomes in α and effects in the ordered ⋆-ring R.

There is intentionally no global Inhabited instance: the zero family satisfies these raw axioms, but using it as an ambient default would silently turn later arguments into vacuous submeasurement statements.

• outcome : α → R
• total : R
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1

structure MIPRE.LIDT.Co.Measurement (α : Type u_1) (R : Type u_2) [Fintype α] [Ring R] [StarRing R] [PartialOrder R] extends MIPRE.LIDT.Co.SubMeas α R : Type (max u_1 u_2)

A paper-local measurement: a POVM whose positive effects sum to the identity.

• outcome : α → R
• total : R
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1
• total_eq_one : self.total = 1

theorem MIPRE.LIDT.Co.Measurement.trivialDistinguishedOutcome_outcome_pos {α : Type u_1} {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ a : α) : 0 ≤ if a = a₀ then 1 else 0

For a trivial distinguished-outcome measurement, every outcome operator is positive: 0 ≤ if a = a₀ then 1 else 0.

noncomputable def MIPRE.LIDT.Co.Measurement.trivialDistinguishedOutcome {α : Type u_1} {R : Type u_2} [Fintype α] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ : α) : Measurement α R

⚠️ DEGENERATE — Construct a trivial measurement where only the distinguished outcome a₀ is the identity and all other outcomes are zero.

This is a valid POVM but highly degenerate: it is only used in vacuous fallback branches of the proof where the error bound is ≥ 1 (see the vendored Test/MainTheorem.lean:mainFormal_trivial_witness).

Call this function explicitly with a chosen outcome. There is intentionally no ambient Inhabited (Measurement α R) instance: choosing a hidden default : α would make degenerate witnesses available to paper-facing existential statements without displaying the selected outcome.

Equations

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

structure MIPRE.LIDT.Co.ProjSubMeas (α : Type u_1) [Fintype α] (R : Type u_2) [Ring R] [StarRing R] [PartialOrder R] extends MIPRE.LIDT.Co.SubMeas α R : Type (max u_1 u_2)

A paper-local projective submeasurement (each effect is idempotent).

There is intentionally no global Inhabited instance: any such default would again collapse to the degenerate zero family.

• outcome : α → R
• total : R
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1
• proj (a : α) : self.outcome a * self.outcome a = self.outcome a

structure MIPRE.LIDT.Co.ProjMeas (α : Type u_1) (R : Type u_2) [Fintype α] [Ring R] [StarRing R] [PartialOrder R] extends MIPRE.LIDT.Co.Measurement α R : Type (max u_1 u_2)

A paper-local projective measurement (complete POVM + projective).

• outcome : α → R
• total : R
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1
• total_eq_one : self.total = 1
• proj (a : α) : self.outcome a * self.outcome a = self.outcome a

theorem MIPRE.LIDT.Co.ProjMeas.trivialDistinguishedOutcome_proj {α : Type u_1} {R : Type u_2} [Fintype α] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ a : α) : (Measurement.trivialDistinguishedOutcome a₀).outcome a * (Measurement.trivialDistinguishedOutcome a₀).outcome a = (Measurement.trivialDistinguishedOutcome a₀).outcome a

For a trivial distinguished-outcome projective measurement, every outcome operator is idempotent.

noncomputable def MIPRE.LIDT.Co.ProjMeas.trivialDistinguishedOutcome {α : Type u_1} {R : Type u_2} [Fintype α] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ : α) : ProjMeas α R

⚠️ DEGENERATE — Construct a trivial projective measurement where only the distinguished outcome a₀ is the identity and all other outcomes are zero.

This is a valid projective POVM but highly degenerate: see the discussion at Measurement.trivialDistinguishedOutcome. As for Measurement, there is intentionally no ambient Inhabited (ProjMeas α R) instance.

Equations

• MIPRE.LIDT.Co.ProjMeas.trivialDistinguishedOutcome a₀ = { toMeasurement := MIPRE.LIDT.Co.Measurement.trivialDistinguishedOutcome a₀, proj := ⋯ }

Derived properties

theorem MIPRE.LIDT.Co.SubMeas.ext {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {A B : SubMeas α R} (houtcome : ∀ (a : α), A.outcome a = B.outcome a) (htotal : A.total = B.total) : A = B

Two submeasurements are equal when they have the same outcome operators and the same total operator.

theorem MIPRE.LIDT.Co.SubMeas.ext_iff {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {A B : SubMeas α R} : A = B ↔ (∀ (a : α), A.outcome a = B.outcome a) ∧ A.total = B.total

theorem MIPRE.LIDT.Co.Measurement.ext {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {A B : Measurement α R} (houtcome : ∀ (a : α), A.outcome a = B.outcome a) : A = B

Two measurements are equal when they have the same outcome operators.

theorem MIPRE.LIDT.Co.Measurement.ext_iff {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {A B : Measurement α R} : A = B ↔ ∀ (a : α), A.outcome a = B.outcome a

theorem MIPRE.LIDT.Co.ProjMeas.ext {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {A B : ProjMeas α R} (houtcome : ∀ (a : α), A.outcome a = B.outcome a) : A = B

Two projective measurements are equal when they have the same outcome operators.

theorem MIPRE.LIDT.Co.ProjMeas.ext_iff {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {A B : ProjMeas α R} : A = B ↔ ∀ (a : α), A.outcome a = B.outcome a

def MIPRE.LIDT.Co.SubMeas.singleOutcome {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : R) (hA_pos : 0 ≤ A) (hA_le_one : A ≤ 1) : SubMeas Unit R

A one-outcome submeasurement associated to a single positive operator bounded by the identity.

Equations

• MIPRE.LIDT.Co.SubMeas.singleOutcome A hA_pos hA_le_one = { outcome := fun (x : Unit) => A, total := A, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := hA_le_one }

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.singleOutcome_outcome {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : R) (hA_pos : 0 ≤ A) (hA_le_one : A ≤ 1) (u : Unit) : (singleOutcome A hA_pos hA_le_one).outcome u = A

The single outcome operator of singleOutcome A is A.

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.singleOutcome_total {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : R) (hA_pos : 0 ≤ A) (hA_le_one : A ≤ 1) : (singleOutcome A hA_pos hA_le_one).total = A

The total of singleOutcome A is A.

theorem MIPRE.LIDT.Co.SubMeas.sum_eq_one_iff_total_eq_one {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : SubMeas α R) : ∑ a : α, A.outcome a = 1 ↔ A.total = 1

A submeasurement is complete exactly when its outcome operators sum to 1.

def MIPRE.LIDT.Co.SubMeas.toMeasurement {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : SubMeas α R) (hcomplete : A.total = 1) : Measurement α R

Promote a complete submeasurement to a measurement.

This is the explicit bridge from the paper's sub-measurement convention ∑ a, A_a ≤ I to the POVM convention ∑ a, A_a = I: callers must supply the completion proof rather than relying on a degenerate default.

Equations

• A.toMeasurement hcomplete = { toSubMeas := A, total_eq_one := hcomplete }

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.toMeasurement_toSubMeas {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : SubMeas α R) (hcomplete : A.total = 1) : (A.toMeasurement hcomplete).toSubMeas = A

Promoting a complete submeasurement and forgetting completeness gives it back.

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.toMeasurement_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (A : SubMeas α R) (hcomplete : A.total = 1) (a : α) : (A.toMeasurement hcomplete).outcome a = A.outcome a

Promotion to a measurement keeps the outcome operators.

theorem MIPRE.LIDT.Co.Measurement.sum_eq {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (M : Measurement α R) : ∑ a : α, M.outcome a = 1

The outcome operators of a measurement sum to the identity.

theorem MIPRE.LIDT.Co.SubMeas.outcome_hermitian {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (A : SubMeas α R) (a : α) : star (A.outcome a) = A.outcome a

Positive outcomes are self-adjoint.

theorem MIPRE.LIDT.Co.Measurement.outcome_hermitian {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : Measurement α R) (a : α) : star (M.outcome a) = M.outcome a

Positive outcomes are self-adjoint.

theorem MIPRE.LIDT.Co.SubMeas.outcome_le_total {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (A : SubMeas α R) (a : α) : A.outcome a ≤ A.total

Every submeasurement outcome is bounded by the total operator.

theorem MIPRE.LIDT.Co.Measurement.outcome_le_one {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : Measurement α R) (a : α) : M.outcome a ≤ 1

Each POVM element is bounded by the identity: outcome a ≤ 1. Proof: outcome a = 1 - ∑_{b ≠ a} outcome b ≤ 1 since all terms are positive.

theorem MIPRE.LIDT.Co.SubMeas.outcome_le_one {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (A : SubMeas α R) (a : α) : A.outcome a ≤ 1

Every submeasurement outcome is bounded by the identity.

theorem MIPRE.LIDT.Co.SubMeas.total_nonneg {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (A : SubMeas α R) : 0 ≤ A.total

The total operator of a submeasurement is positive.

theorem MIPRE.LIDT.Co.ProjSubMeas.outcome_hermitian {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : ProjSubMeas α R) (a : α) : star (P.outcome a) = P.outcome a

Projective submeasurement outcomes are self-adjoint (positive by assumption).

theorem MIPRE.LIDT.Co.ProjMeas.outcome_hermitian {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : ProjMeas α R) (a : α) : star (P.outcome a) = P.outcome a

Projective measurement outcomes are self-adjoint (inherited from Measurement.outcome_pos).

Projective submeasurements in a C*-algebra

theorem MIPRE.LIDT.Co.ProjSubMeas.outcome_mul_total_eq_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjSubMeas α R) (a : α) : P.outcome a * P.total = P.outcome a

Each projective outcome is absorbed by the total operator.

theorem MIPRE.LIDT.Co.ProjSubMeas.total_proj {α : Type u_1} [Fintype α] {R : Type u_2} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjSubMeas α R) : P.total * P.total = P.total

The total operator of a projective submeasurement is itself a projector.

theorem MIPRE.LIDT.Co.ProjSubMeas.outcome_orthogonal {α : Type u_1} [Fintype α] {R : Type u_2} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjSubMeas α R) (a b : α) (hab : a ≠ b) : P.outcome a * P.outcome b = 0

Distinct outcomes of a projective submeasurement are orthogonal.

theorem MIPRE.LIDT.Co.ProjMeas.outcome_orthogonal {α : Type u_1} [Fintype α] {R : Type u_2} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjMeas α R) (a b : α) (hab : a ≠ b) : P.outcome a * P.outcome b = 0

Distinct outcomes of a projective measurement are orthogonal.

theorem MIPRE.LIDT.Co.ProjMeas.outcome_commute {α : Type u_1} [Fintype α] {R : Type u_2} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjMeas α R) (a b : α) : P.outcome a * P.outcome b = P.outcome b * P.outcome a

Any two outcomes of a ProjMeas commute.

Images under ⋆-homomorphisms

The port's placement of a local family on a tensor factor: A.map S.L is the vendored SubMeas.liftLeft A, and A.map S.R the vendored SubMeas.liftRight A.

def MIPRE.LIDT.Co.SubMeas.map {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (A : SubMeas α R) : SubMeas α T

The image of a submeasurement under a ⋆-algebra homomorphism.

Equations

• MIPRE.LIDT.Co.SubMeas.map f A = { outcome := fun (a : α) => f (A.outcome a), total := f A.total, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.map_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (A : SubMeas α R) (a : α) : (map f A).outcome a = f (A.outcome a)

The outcome operators of the image are the images of the outcome operators.

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.map_total {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (A : SubMeas α R) : (map f A).total = f A.total

The total of the image is the image of the total.

def MIPRE.LIDT.Co.Measurement.map {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (M : Measurement α R) : Measurement α T

The image of a measurement under a ⋆-algebra homomorphism.

Equations

• MIPRE.LIDT.Co.Measurement.map f M = { toSubMeas := MIPRE.LIDT.Co.SubMeas.map f M.toSubMeas, total_eq_one := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.Measurement.map_toSubMeas {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (M : Measurement α R) : (map f M).toSubMeas = SubMeas.map f M.toSubMeas

The image of a measurement, as a submeasurement, is the image of its submeasurement.

@[simp]

theorem MIPRE.LIDT.Co.Measurement.map_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (M : Measurement α R) (a : α) : (map f M).outcome a = f (M.outcome a)

The outcome operators of the image measurement are the images of the outcome operators.

def MIPRE.LIDT.Co.ProjSubMeas.map {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (P : ProjSubMeas α R) : ProjSubMeas α T

The image of a projective submeasurement under a ⋆-algebra homomorphism.

Equations

• MIPRE.LIDT.Co.ProjSubMeas.map f P = { toSubMeas := MIPRE.LIDT.Co.SubMeas.map f P.toSubMeas, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.ProjSubMeas.map_toSubMeas {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (P : ProjSubMeas α R) : (map f P).toSubMeas = SubMeas.map f P.toSubMeas

The image of a projective submeasurement, as a submeasurement, is the image of its submeasurement.

def MIPRE.LIDT.Co.ProjMeas.map {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (P : ProjMeas α R) : ProjMeas α T

The image of a projective measurement under a ⋆-algebra homomorphism.

Equations

• MIPRE.LIDT.Co.ProjMeas.map f P = { toMeasurement := MIPRE.LIDT.Co.Measurement.map f P.toMeasurement, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.ProjMeas.map_toMeasurement {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_3} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (f : R →⋆ₐ[ℂ] T) (P : ProjMeas α R) : (map f P).toMeasurement = Measurement.map f P.toMeasurement

The image of a projective measurement, as a measurement, is the image of its measurement.

Bridges to MIPRE.POVMIn and MIPRE.IsPVMIn

def MIPRE.LIDT.Co.Measurement.ofPOVMIn {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (P : POVMIn α R) : Measurement α R

A positive operator valued measure of the repository as a measurement.

Equations

• MIPRE.LIDT.Co.Measurement.ofPOVMIn P = { outcome := P.op, total := 1, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯, total_eq_one := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.Measurement.ofPOVMIn_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] (P : POVMIn α R) (a : α) : (ofPOVMIn P).outcome a = P.op a

The outcome operators of ofPOVMIn P are the operators of P.

def MIPRE.LIDT.Co.Measurement.toPOVMIn {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : Measurement α R) : POVMIn α R

A measurement as a positive operator valued measure of the repository (MIPRE/Foundations/Measurement.lean).

Equations

• M.toPOVMIn = { mats := fun (a : α) => ⟨M.outcome a, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.Measurement.toPOVMIn_op {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : Measurement α R) (a : α) : M.toPOVMIn.op a = M.outcome a

The operators of toPOVMIn M are the outcome operators of M.

@[simp]

theorem MIPRE.LIDT.Co.Measurement.ofPOVMIn_toPOVMIn {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : Measurement α R) : ofPOVMIn M.toPOVMIn = M

ofPOVMIn is a left inverse of toPOVMIn.

@[simp]

theorem MIPRE.LIDT.Co.Measurement.toPOVMIn_ofPOVMIn {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : POVMIn α R) : (ofPOVMIn P).toPOVMIn = P

toPOVMIn is a left inverse of ofPOVMIn.

def MIPRE.LIDT.Co.ProjMeas.ofIsPVMIn {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : α → R) (h : IsPVMIn P) : ProjMeas α R

A family of self-adjoint idempotents summing to one, mutually orthogonal, as a projective measurement.

Equations

• MIPRE.LIDT.Co.ProjMeas.ofIsPVMIn P h = { outcome := P, total := 1, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯, total_eq_one := ⋯, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.ProjMeas.ofIsPVMIn_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : α → R) (h : IsPVMIn P) (a : α) : (ofIsPVMIn P h).outcome a = P a

The outcome operators of ofIsPVMIn P h are the P a.

theorem MIPRE.LIDT.Co.ProjMeas.isPVMIn {α : Type u_1} [Fintype α] {R : Type u_2} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjMeas α R) : IsPVMIn P.outcome

A projective measurement is a projective measurement of the repository (MIPRE/Foundations/Measurement.lean): orthogonality is ProjSubMeas.outcome_orthogonal.