Heterogeneous role-register measurement extraction

This file contains the principal-block extraction used to unsymmetrize a measurement on the heterogeneous role-register space Role × (ιA ⊕ ιB). The Alice extraction is the block indexed by (Role.A, Sum.inl _); the Bob extraction is the block indexed by (Role.B, Sum.inr _).

These are the two-space analogues of the same-space extractions in MIPStarRE.LDT.Test.Unsymmetrization. They preserve POVM completeness, but they do not assert that arbitrary principal blocks of a projective measurement remain projective. As in the paper proof, projectivity is restored later by the projectivization step.

References

• references/ldt-paper/inductive_step.tex, lines 84--109.

Principal blocks of heterogeneous role-register operators

noncomputable def MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock {ιA : Type u_1} {ιB : Type u_2} (Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : Quantum.Op ιA

Alice's principal block of an operator on the heterogeneous role-register space, indexed by (Role.A, Sum.inl _).

Equations

• MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock Y = Matrix.submatrix Y (fun (i : ιA) => (MIPStarRE.LDT.Role.A, Sum.inl i)) fun (i : ιA) => (MIPStarRE.LDT.Role.A, Sum.inl i)

noncomputable def MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock {ιA : Type u_1} {ιB : Type u_2} (Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : Quantum.Op ιB

Bob's principal block of an operator on the heterogeneous role-register space, indexed by (Role.B, Sum.inr _).

Equations

• MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock Y = Matrix.submatrix Y (fun (i : ιB) => (MIPStarRE.LDT.Role.B, Sum.inr i)) fun (i : ιB) => (MIPStarRE.LDT.Role.B, Sum.inr i)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_apply {ιA : Type u_1} {ιB : Type u_2} (Y : Quantum.Op (RoleRegisterLocal ιA ιB)) (i j : ιA) : extractRoleRegisterAliceBlock Y i j = Y (Role.A, Sum.inl i) (Role.A, Sum.inl j)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_apply {ιA : Type u_1} {ιB : Type u_2} (Y : Quantum.Op (RoleRegisterLocal ιA ιB)) (i j : ιB) : extractRoleRegisterBobBlock Y i j = Y (Role.B, Sum.inr i) (Role.B, Sum.inr j)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_zero {ιA : Type u_1} {ιB : Type u_2} : extractRoleRegisterAliceBlock 0 = 0

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_zero {ιA : Type u_1} {ιB : Type u_2} : extractRoleRegisterBobBlock 0 = 0

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_add {ιA : Type u_1} {ιB : Type u_2} (X Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterAliceBlock (X + Y) = extractRoleRegisterAliceBlock X + extractRoleRegisterAliceBlock Y

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_add {ιA : Type u_1} {ιB : Type u_2} (X Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterBobBlock (X + Y) = extractRoleRegisterBobBlock X + extractRoleRegisterBobBlock Y

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_sub {ιA : Type u_1} {ιB : Type u_2} (X Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterAliceBlock (X - Y) = extractRoleRegisterAliceBlock X - extractRoleRegisterAliceBlock Y

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_sub {ιA : Type u_1} {ιB : Type u_2} (X Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterBobBlock (X - Y) = extractRoleRegisterBobBlock X - extractRoleRegisterBobBlock Y

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_smul {ιA : Type u_1} {ιB : Type u_2} (c : ℂ) (Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterAliceBlock (c • Y) = c • extractRoleRegisterAliceBlock Y

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_smul {ιA : Type u_1} {ιB : Type u_2} (c : ℂ) (Y : Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterBobBlock (c • Y) = c • extractRoleRegisterBobBlock Y

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_finset_sum {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} (s : Finset α) (f : α → Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterAliceBlock (∑ a ∈ s, f a) = ∑ a ∈ s, extractRoleRegisterAliceBlock (f a)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_finset_sum {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} (s : Finset α) (f : α → Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterBobBlock (∑ a ∈ s, f a) = ∑ a ∈ s, extractRoleRegisterBobBlock (f a)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_univ_sum {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] (f : α → Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterAliceBlock (∑ a : α, f a) = ∑ a : α, extractRoleRegisterAliceBlock (f a)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_univ_sum {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] (f : α → Quantum.Op (RoleRegisterLocal ιA ιB)) : extractRoleRegisterBobBlock (∑ a : α, f a) = ∑ a : α, extractRoleRegisterBobBlock (f a)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_one {ιA : Type u_1} {ιB : Type u_2} [DecidableEq ιA] [DecidableEq ιB] : extractRoleRegisterAliceBlock 1 = 1

@[simp]

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_one {ιA : Type u_1} {ιB : Type u_2} [DecidableEq ιA] [DecidableEq ιB] : extractRoleRegisterBobBlock 1 = 1

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_nonneg {ιA : Type u_1} {ιB : Type u_2} {Y : Quantum.Op (RoleRegisterLocal ιA ιB)} (hY : 0 ≤ Y) : 0 ≤ extractRoleRegisterAliceBlock Y

Alice principal blocks preserve positive semidefiniteness.

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_nonneg {ιA : Type u_1} {ιB : Type u_2} {Y : Quantum.Op (RoleRegisterLocal ιA ιB)} (hY : 0 ≤ Y) : 0 ≤ extractRoleRegisterBobBlock Y

Bob principal blocks preserve positive semidefiniteness.

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterAliceBlock_le {ιA : Type u_1} {ιB : Type u_2} {X Y : Quantum.Op (RoleRegisterLocal ιA ιB)} (hXY : X ≤ Y) : extractRoleRegisterAliceBlock X ≤ extractRoleRegisterAliceBlock Y

Alice principal blocks are monotone for the matrix order.

theorem MIPStarRE.LDT.ProjStrat.extractRoleRegisterBobBlock_le {ιA : Type u_1} {ιB : Type u_2} {X Y : Quantum.Op (RoleRegisterLocal ιA ιB)} (hXY : X ≤ Y) : extractRoleRegisterBobBlock X ≤ extractRoleRegisterBobBlock Y

Bob principal blocks are monotone for the matrix order.

noncomputable def MIPStarRE.LDT.SubMeas.extractRoleRegisterAlice {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) : SubMeas α ιA

Extract Alice's original local block from a submeasurement on the heterogeneous role-register space.

Equations

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

noncomputable def MIPStarRE.LDT.SubMeas.extractRoleRegisterBob {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) : SubMeas α ιB

Extract Bob's original local block from a submeasurement on the heterogeneous role-register space.

Equations

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

@[simp]

theorem MIPStarRE.LDT.SubMeas.extractRoleRegisterAlice_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) (a : α) : A.extractRoleRegisterAlice.outcome a = ProjStrat.extractRoleRegisterAliceBlock (A.outcome a)

@[simp]

theorem MIPStarRE.LDT.SubMeas.extractRoleRegisterBob_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) (a : α) : A.extractRoleRegisterBob.outcome a = ProjStrat.extractRoleRegisterBobBlock (A.outcome a)

@[simp]

theorem MIPStarRE.LDT.SubMeas.extractRoleRegisterAlice_total {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) : A.extractRoleRegisterAlice.total = ProjStrat.extractRoleRegisterAliceBlock A.total

@[simp]

theorem MIPStarRE.LDT.SubMeas.extractRoleRegisterBob_total {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) : A.extractRoleRegisterBob.total = ProjStrat.extractRoleRegisterBobBlock A.total

theorem MIPStarRE.LDT.SubMeas.extractRoleRegisterAlice_postprocess {α : Type u_1} {β : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype α] [Fintype β] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) (f : α → β) : (postprocess A f).extractRoleRegisterAlice = postprocess A.extractRoleRegisterAlice f

Alice extraction commutes with outcome postprocessing.

theorem MIPStarRE.LDT.SubMeas.extractRoleRegisterBob_postprocess {α : Type u_1} {β : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype α] [Fintype β] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : SubMeas α (ProjStrat.RoleRegisterLocal ιA ιB)) (f : α → β) : (postprocess A f).extractRoleRegisterBob = postprocess A.extractRoleRegisterBob f

Bob extraction commutes with outcome postprocessing.

noncomputable def MIPStarRE.LDT.Measurement.extractRoleRegisterAlice {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Measurement α (ProjStrat.RoleRegisterLocal ιA ιB)) : Measurement α ιA

Extract Alice's original local block from a measurement on the heterogeneous role-register space.

Equations

• A.extractRoleRegisterAlice = { toSubMeas := A.extractRoleRegisterAlice, total_eq_one := ⋯ }

noncomputable def MIPStarRE.LDT.Measurement.extractRoleRegisterBob {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Measurement α (ProjStrat.RoleRegisterLocal ιA ιB)) : Measurement α ιB

Extract Bob's original local block from a measurement on the heterogeneous role-register space.

Equations

• A.extractRoleRegisterBob = { toSubMeas := A.extractRoleRegisterBob, total_eq_one := ⋯ }

@[simp]

theorem MIPStarRE.LDT.Measurement.extractRoleRegisterAlice_toSubMeas {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Measurement α (ProjStrat.RoleRegisterLocal ιA ιB)) : A.extractRoleRegisterAlice.toSubMeas = A.extractRoleRegisterAlice

@[simp]

theorem MIPStarRE.LDT.Measurement.extractRoleRegisterBob_toSubMeas {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Measurement α (ProjStrat.RoleRegisterLocal ιA ιB)) : A.extractRoleRegisterBob.toSubMeas = A.extractRoleRegisterBob

@[simp]

theorem MIPStarRE.LDT.Measurement.extractRoleRegisterAlice_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Measurement α (ProjStrat.RoleRegisterLocal ιA ιB)) (a : α) : A.extractRoleRegisterAlice.outcome a = ProjStrat.extractRoleRegisterAliceBlock (A.outcome a)

@[simp]

theorem MIPStarRE.LDT.Measurement.extractRoleRegisterBob_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Measurement α (ProjStrat.RoleRegisterLocal ιA ιB)) (a : α) : A.extractRoleRegisterBob.outcome a = ProjStrat.extractRoleRegisterBobBlock (A.outcome a)

Extraction on the constructed role-register measurements

Trace compression for occupied role-register sectors

theorem MIPStarRE.LDT.ProjStrat.qBipartiteMatchMass_roleRegisterProjMeas_arbitrary_eq_average {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (G : Measurement Outcome (RoleRegisterLocal ιA ιB)) : qBipartiteMatchMass (roleRegisterSymmState ψ) (roleRegisterProjMeas MA MB).toSubMeas G.toSubMeas = (qBipartiteMatchMass ψ MA.toSubMeas G.extractRoleRegisterBob.toSubMeas + qBipartiteMatchMass ψ G.extractRoleRegisterAlice.toSubMeas MB.toSubMeas) / 2

Match-mass identity for a heterogeneous role-register measurement against an arbitrary measurement on the role-register space.

theorem MIPStarRE.LDT.ProjStrat.qBipartiteConsDefect_roleRegisterProjMeas_arbitrary_eq_average {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (G : Measurement Outcome (RoleRegisterLocal ιA ιB)) : qBipartiteConsDefect (roleRegisterSymmState ψ) (roleRegisterProjMeas MA MB).toSubMeas G.toSubMeas = (qBipartiteConsDefect ψ MA.toSubMeas G.extractRoleRegisterBob.toSubMeas + qBipartiteConsDefect ψ G.extractRoleRegisterAlice.toSubMeas MB.toSubMeas) / 2

Questionwise consistency identity for extracting the two occupied principal blocks from an arbitrary heterogeneous role-register measurement.

theorem MIPStarRE.LDT.ProjStrat.qBipartiteConsDefect_extractRoleRegisterBob_le_two_symm {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (G : Measurement Outcome (RoleRegisterLocal ιA ιB)) : qBipartiteConsDefect ψ MA.toSubMeas G.extractRoleRegisterBob.toSubMeas ≤ 2 * qBipartiteConsDefect (roleRegisterSymmState ψ) (roleRegisterProjMeas MA MB).toSubMeas G.toSubMeas

One heterogeneous questionwise factor-two consequence of the role-register unsymmetrization identity.

theorem MIPStarRE.LDT.ProjStrat.qBipartiteConsDefect_extractRoleRegisterAlice_le_two_symm {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (G : Measurement Outcome (RoleRegisterLocal ιA ιB)) : qBipartiteConsDefect ψ G.extractRoleRegisterAlice.toSubMeas MB.toSubMeas ≤ 2 * qBipartiteConsDefect (roleRegisterSymmState ψ) (roleRegisterProjMeas MA MB).toSubMeas G.toSubMeas

The other heterogeneous questionwise factor-two consequence of the role-register unsymmetrization identity.

theorem MIPStarRE.LDT.ProjStrat.polynomialEvaluationFamily_extractRoleRegisterAlice {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (G : SubMeas (Polynomial params) (RoleRegisterLocal ιA ιB)) : polynomialEvaluationFamily params G.extractRoleRegisterAlice = fun (u : Point params) => (polynomialEvaluationFamily params G u).extractRoleRegisterAlice

Polynomial evaluation commutes with Alice extraction from a heterogeneous role-register polynomial submeasurement.

theorem MIPStarRE.LDT.ProjStrat.polynomialEvaluationFamily_extractRoleRegisterBob {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (G : SubMeas (Polynomial params) (RoleRegisterLocal ιA ιB)) : polynomialEvaluationFamily params G.extractRoleRegisterBob = fun (u : Point params) => (polynomialEvaluationFamily params G u).extractRoleRegisterBob

Polynomial evaluation commutes with Bob extraction from a heterogeneous role-register polynomial submeasurement.

theorem MIPStarRE.LDT.ProjStrat.polynomialEvaluationFamily_measurement_extractRoleRegisterAlice {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (G : Measurement (Polynomial params) (RoleRegisterLocal ιA ιB)) : polynomialEvaluationFamily params G.extractRoleRegisterAlice.toSubMeas = fun (u : Point params) => (polynomialEvaluationFamily params G.toSubMeas u).extractRoleRegisterAlice

Measurement-level form of polynomialEvaluationFamily_extractRoleRegisterAlice.

theorem MIPStarRE.LDT.ProjStrat.polynomialEvaluationFamily_measurement_extractRoleRegisterBob {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (G : Measurement (Polynomial params) (RoleRegisterLocal ιA ιB)) : polynomialEvaluationFamily params G.extractRoleRegisterBob.toSubMeas = fun (u : Point params) => (polynomialEvaluationFamily params G.toSubMeas u).extractRoleRegisterBob

Measurement-level form of polynomialEvaluationFamily_extractRoleRegisterBob.