Indexed and bipartite submeasurement infrastructure

Indexed measurement families, tensor placements, and lift/placement constructors.

Indexed measurement families

@[reducible, inline]

abbrev MIPStarRE.LDT.IdxSubMeas (Question : Type u_1) (Outcome : Type u_2) (ι : Type u_3) [Fintype Outcome] [Fintype ι] [DecidableEq ι] : Type (max (max u_1 u_3) u_2)

Question-indexed family of submeasurements.

Equations

• MIPStarRE.LDT.IdxSubMeas Question Outcome ι = (Question → MIPStarRE.LDT.SubMeas Outcome ι)

@[reducible, inline]

abbrev MIPStarRE.LDT.IdxMeas (Question : Type u_1) (Outcome : Type u_2) (ι : Type u_3) [Fintype Outcome] [Fintype ι] [DecidableEq ι] : Type (max (max u_1 u_3) u_2)

Question-indexed family of measurements.

Equations

• MIPStarRE.LDT.IdxMeas Question Outcome ι = (Question → MIPStarRE.LDT.Measurement Outcome ι)

@[reducible, inline]

abbrev MIPStarRE.LDT.IdxProjSubMeas (Question : Type u_1) (Outcome : Type u_2) (ι : Type u_3) [Fintype Outcome] [Fintype ι] [DecidableEq ι] : Type (max (max u_1 u_3) u_2)

Question-indexed family of projective submeasurements.

Equations

• MIPStarRE.LDT.IdxProjSubMeas Question Outcome ι = (Question → MIPStarRE.LDT.ProjSubMeas Outcome ι)

@[reducible, inline]

abbrev MIPStarRE.LDT.IdxProjMeas (Question : Type u_1) (Outcome : Type u_2) (ι : Type u_3) [Fintype Outcome] [Fintype ι] [DecidableEq ι] : Type (max (max u_1 u_3) u_2)

Question-indexed family of projective measurements.

Equations

• MIPStarRE.LDT.IdxProjMeas Question Outcome ι = (Question → MIPStarRE.LDT.ProjMeas Outcome ι)

def MIPStarRE.LDT.IdxMeas.toIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxMeas Question Outcome ι) : IdxSubMeas Question Outcome ι

Forget completeness from an indexed measurement family.

Equations

• A.toIdxSubMeas q = (A q).toSubMeas

def MIPStarRE.LDT.IdxProjSubMeas.toIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxProjSubMeas Question Outcome ι) : IdxSubMeas Question Outcome ι

Forget projectivity from an indexed projective submeasurement family.

Equations

• A.toIdxSubMeas q = (A q).toSubMeas

def MIPStarRE.LDT.IdxProjMeas.toIdxMeas {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxProjMeas Question Outcome ι) : IdxMeas Question Outcome ι

Forget projectivity from an indexed projective measurement family.

Equations

• A.toIdxMeas q = (A q).toMeasurement

def MIPStarRE.LDT.IdxProjMeas.toIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxProjMeas Question Outcome ι) : IdxSubMeas Question Outcome ι

Forget both projectivity and completeness from an indexed projective measurement family.

Equations

• A.toIdxSubMeas q = (A q).toSubMeas

noncomputable def MIPStarRE.LDT.postprocess {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype α] [Fintype β] (A : SubMeas α ι) (f : α → β) : SubMeas β ι

Post-process the outcomes of a submeasurement. The processed operator at b is the sum of the operators of all a with f a = b.

Equations

• MIPStarRE.LDT.postprocess A f = { outcome := fun (b : β) => ∑ a : α with f a = b, A.outcome a, total := A.total, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯ }

@[simp]

theorem MIPStarRE.LDT.SubMeas.postprocess_outcome {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq β] [DecidableEq ι] (A : SubMeas α ι) (f : α → β) (b : β) : (postprocess A f).outcome b = ∑ a : α with f a = b, A.outcome a

The outcome of a postprocessed submeasurement is the sum over the fiber of the readout map.

@[simp]

theorem MIPStarRE.LDT.SubMeas.postprocess_id {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : (postprocess A fun (a : α) => a) = A

Postprocessing a submeasurement by the identity readout leaves it unchanged.

noncomputable def MIPStarRE.LDT.SubMeas.transport {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : SubMeas α ι) : SubMeas β ι

Transport a submeasurement along an equivalence of outcome types.

Equations

• MIPStarRE.LDT.SubMeas.transport e A = { outcome := fun (b : β) => A.outcome (e.symm b), total := A.total, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯ }

@[simp]

theorem MIPStarRE.LDT.SubMeas.transport_outcome {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : SubMeas α ι) (b : β) : (transport e A).outcome b = A.outcome (e.symm b)

@[simp]

theorem MIPStarRE.LDT.SubMeas.transport_total {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : SubMeas α ι) : (transport e A).total = A.total

theorem MIPStarRE.LDT.SubMeas.postprocess_transport {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : SubMeas α ι) (f : β → γ) : postprocess (transport e A) f = postprocess A fun (a : α) => f (e a)

Postprocessing after transporting outcomes along an equivalence agrees with postprocessing the original submeasurement after precomposing the readout map with the same equivalence.

theorem MIPStarRE.LDT.SubMeas.postprocess_transport_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ι : Type u_5} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] [Fintype ι] [DecidableEq ι] (eα : α ≃ β) (eγ : γ ≃ δ) (A : SubMeas α ι) (f : α → γ) (g : β → δ) (h : ∀ (a : α), g (eα a) = eγ (f a)) : postprocess (transport eα A) g = transport eγ (postprocess A f)

Naturality of postprocessing with respect to transport along equivalences on both the source and target outcome alphabets.

@[simp]

theorem MIPStarRE.LDT.SubMeas.postprocess_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (f : α → β) (g : β → γ) : postprocess (postprocess A f) g = postprocess A fun (a : α) => g (f a)

Postprocessing is functorial: postprocessing by f and then by g agrees with a single postprocessing by the composite g ∘ f.

noncomputable def MIPStarRE.LDT.Measurement.transport {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : Measurement α ι) : Measurement β ι

Transport a measurement along an equivalence of outcome types.

Equations

• MIPStarRE.LDT.Measurement.transport e A = { toSubMeas := MIPStarRE.LDT.SubMeas.transport e A.toSubMeas, total_eq_one := ⋯ }

noncomputable def MIPStarRE.LDT.ProjSubMeas.transport {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : ProjSubMeas α ι) : ProjSubMeas β ι

Transport a projective submeasurement along an equivalence of outcome types.

Equations

• MIPStarRE.LDT.ProjSubMeas.transport e A = { toSubMeas := MIPStarRE.LDT.SubMeas.transport e A.toSubMeas, proj := ⋯ }

theorem MIPStarRE.LDT.ProjSubMeas.postprocess_outcome_proj {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas α ι) (f : α → β) (b : β) : (postprocess P.toSubMeas f).outcome b * (postprocess P.toSubMeas f).outcome b = (postprocess P.toSubMeas f).outcome b

Postprocessing a projective submeasurement preserves outcome projectivity.

noncomputable def MIPStarRE.LDT.ProjMeas.transport {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : ProjMeas α ι) : ProjMeas β ι

Transport a projective measurement along an equivalence of outcome types.

Equations

• MIPStarRE.LDT.ProjMeas.transport e A = { toMeasurement := MIPStarRE.LDT.Measurement.transport e A.toMeasurement, proj := ⋯ }

@[simp]

theorem MIPStarRE.LDT.ProjMeas.transport_trivialDistinguishedOutcome {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (e : α ≃ α) (a₀ : α) : transport e (trivialDistinguishedOutcome a₀) = trivialDistinguishedOutcome (e a₀)

@[simp]

theorem MIPStarRE.LDT.ProjMeas.transport_toSubMeas {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (e : α ≃ β) (A : ProjMeas α ι) : (transport e A).toSubMeas = SubMeas.transport e A.toSubMeas

noncomputable def MIPStarRE.LDT.ProjMeas.postprocess {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (A : ProjMeas α ι) (f : α → β) : ProjMeas β ι

Postprocess a projective measurement along a relabeling of the outcome type.

The fiber of each output value is a sum of mutually orthogonal projectors, so postprocessing preserves projectivity as well as completeness.

Equations

• A.postprocess f = { toMeasurement := let __SubMeas := MIPStarRE.LDT.postprocess A.toSubMeas f; { toSubMeas := __SubMeas, total_eq_one := ⋯ }, proj := ⋯ }

@[simp]

theorem MIPStarRE.LDT.ProjMeas.postprocess_toSubMeas {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (A : ProjMeas α ι) (f : α → β) : (A.postprocess f).toSubMeas = LDT.postprocess A.toSubMeas f

theorem MIPStarRE.LDT.ProjMeas.postprocess_outcome_commute {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [Fintype ι] [DecidableEq ι] (P : ProjMeas α ι) (f : α → β) (g : α → γ) (b : β) (c : γ) : (LDT.postprocess P.toSubMeas f).outcome b * (LDT.postprocess P.toSubMeas g).outcome c = (LDT.postprocess P.toSubMeas g).outcome c * (LDT.postprocess P.toSubMeas f).outcome b

Postprocessed outcomes from the same ProjMeas commute.

noncomputable def MIPStarRE.LDT.completeSubMeas {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : Measurement (Option α) ι

Complete a submeasurement by adjoining a distinguished failure outcome.

Equations

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

def MIPStarRE.LDT.constSubMeasFamily {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : IdxSubMeas Unit α ι

Constant indexed family taking the same submeasurement on every question.

Equations

• MIPStarRE.LDT.constSubMeasFamily A x✝ = A

noncomputable def MIPStarRE.LDT.averageIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} [Fintype Outcome] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : SubMeas Outcome ι

Average an indexed submeasurement family against a finite distribution.

The hypothesis ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1 says that 𝒟 is a sub-probability distribution (total mass at most 1); this is all that is needed to keep the averaged total operator below 1.

Equations

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

Tensor-placement constructors

@[simp]

theorem MIPStarRE.LDT.mkLeftPlacedSubMeas_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιA) (a : α) : (MIPStarRE.LDT.mkLeftPlacedSubMeas✝ A).outcome a = leftTensor (A.outcome a)

Helper-level projection equation for left-placed outcomes.

@[simp]

theorem MIPStarRE.LDT.mkLeftPlacedSubMeas_total {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιA) : (MIPStarRE.LDT.mkLeftPlacedSubMeas✝ A).total = leftTensor A.total

Helper-level projection equation for left-placed totals.

@[simp]

theorem MIPStarRE.LDT.mkRightPlacedSubMeas_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιB) (a : α) : (MIPStarRE.LDT.mkRightPlacedSubMeas✝ A).outcome a = rightTensor (A.outcome a)

Helper-level projection equation for right-placed outcomes.

@[simp]

theorem MIPStarRE.LDT.mkRightPlacedSubMeas_total {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιB) : (MIPStarRE.LDT.mkRightPlacedSubMeas✝ A).total = rightTensor A.total

Helper-level projection equation for right-placed totals.

Square bipartite lifts

def MIPStarRE.LDT.SubMeas.liftLeft {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : SubMeas α (ι × ι)

Lift a submeasurement to the left tensor factor of a bipartite space ι × ι. Each outcome operator A_a : Op ι becomes A_a ⊗ I : Op (ι × ι).

Equations

• A.liftLeft = MIPStarRE.LDT.mkLeftPlacedSubMeas✝ A

def MIPStarRE.LDT.IdxSubMeas.liftLeft {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxSubMeas Question Outcome ι) : IdxSubMeas Question Outcome (ι × ι)

Lift an indexed submeasurement family to the left tensor factor.

Equations

• A.liftLeft q = MIPStarRE.LDT.mkLeftPlacedSubMeas✝ (A q)

def MIPStarRE.LDT.ProjSubMeas.liftLeft {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : ProjSubMeas α ι) : ProjSubMeas α (ι × ι)

Lift a projective submeasurement to the left tensor factor of a bipartite space ι × ι.

Equations

• A.liftLeft = { toSubMeas := A.liftLeft, proj := ⋯ }

def MIPStarRE.LDT.SubMeas.liftRight {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : SubMeas α (ι × ι)

Lift a submeasurement to the right tensor factor of a bipartite space ι × ι. Each outcome operator A_a : Op ι becomes I ⊗ A_a : Op (ι × ι).

Equations

• A.liftRight = MIPStarRE.LDT.mkRightPlacedSubMeas✝ A

def MIPStarRE.LDT.IdxSubMeas.liftRight {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxSubMeas Question Outcome ι) : IdxSubMeas Question Outcome (ι × ι)

Lift an indexed submeasurement family to the right tensor factor.

Equations

• A.liftRight q = MIPStarRE.LDT.mkRightPlacedSubMeas✝ (A q)

General bipartite placement

def MIPStarRE.LDT.leftPlacedSubMeas {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιA) : SubMeas α (ιA × ιB)

Place a submeasurement on the left tensor factor of ιA × ιB.

Equations

• MIPStarRE.LDT.leftPlacedSubMeas A = MIPStarRE.LDT.mkLeftPlacedSubMeas✝ A

@[simp]

theorem MIPStarRE.LDT.leftPlacedSubMeas_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιA) (a : α) : (leftPlacedSubMeas A).outcome a = leftTensor (A.outcome a)

Outcome operators of a left-placed submeasurement are left tensor placements.

@[simp]

theorem MIPStarRE.LDT.leftPlacedSubMeas_total {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιA) : (leftPlacedSubMeas A).total = leftTensor A.total

The total operator of a left-placed submeasurement is a left tensor placement.

def MIPStarRE.LDT.rightPlacedSubMeas {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιB) : SubMeas α (ιA × ιB)

Place a submeasurement on the right tensor factor of ιA × ιB.

Equations

• MIPStarRE.LDT.rightPlacedSubMeas A = MIPStarRE.LDT.mkRightPlacedSubMeas✝ A

@[simp]

theorem MIPStarRE.LDT.rightPlacedSubMeas_outcome {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιB) (a : α) : (rightPlacedSubMeas A).outcome a = rightTensor (A.outcome a)

Outcome operators of a right-placed submeasurement are right tensor placements.

@[simp]

theorem MIPStarRE.LDT.rightPlacedSubMeas_total {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (A : SubMeas α ιB) : (rightPlacedSubMeas A).total = rightTensor A.total

The total operator of a right-placed submeasurement is a right tensor placement.

def MIPStarRE.LDT.IdxSubMeas.placeLeft {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (A : IdxSubMeas Question Outcome ιA) : IdxSubMeas Question Outcome (ιA × ιB)

Lift an indexed submeasurement family to the left tensor factor of ιA × ιB (general bipartite placement).

Equations

• A.placeLeft q = MIPStarRE.LDT.mkLeftPlacedSubMeas✝ (A q)

def MIPStarRE.LDT.IdxSubMeas.placeRight {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (A : IdxSubMeas Question Outcome ιB) : IdxSubMeas Question Outcome (ιA × ιB)

Lift an indexed submeasurement family to the right tensor factor of ιA × ιB (general bipartite placement).

Equations

• A.placeRight q = MIPStarRE.LDT.mkRightPlacedSubMeas✝ (A q)