Indexed and bipartite submeasurement infrastructure

Indexed measurement families, tensor placements, and lift/placement constructors: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

As in Co/Basic/SubMeasurementCore.lean, the families are generic over an ordered ⋆-ring R (the vendored Op ι): local families take R = 𝔓, joint ones R = K →L[ℂ] K. Each declaration asks for what its proof uses: [StarOrderedRing R] for the positivity of postprocessed and completed outcomes, a C*-algebra for the projective postprocessing (through the orthogonality ProjSubMeas.outcome_orthogonal), and the real ordered-module structure of averageOperatorOverDistribution for averageIdxSubMeas.

The placements take the symmetric model S as an argument, in place of the vendored named carriers (ιA := ιA), (ιB := ιB): a local family is placed on the first or second factor by SubMeas.map along S.L or S.R (Co/Basic/SubMeasurementCore.lean), so S.mkLeftPlacedSubMeas A = A.map S.L and (A.liftLeft S).outcome a = S.L (A.outcome a) hold by rfl. The square and the general bipartite placements of the vendored file coincide here, since the model has one local algebra.

Not ported

Every declaration of the vendored file has a counterpart here.

Indexed measurement families

@[reducible, inline]

abbrev MIPRE.LIDT.Co.IdxSubMeas (Question : Type u_1) (Outcome : Type u_2) (R : Type u_3) [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] : Type (max (max u_1 u_3) u_2)

Question-indexed family of submeasurements.

Equations

• MIPRE.LIDT.Co.IdxSubMeas Question Outcome R = (Question → MIPRE.LIDT.Co.SubMeas Outcome R)

@[reducible, inline]

abbrev MIPRE.LIDT.Co.IdxMeas (Question : Type u_1) (Outcome : Type u_2) (R : Type u_3) [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] : Type (max (max u_1 u_3) u_2)

Question-indexed family of measurements.

Equations

• MIPRE.LIDT.Co.IdxMeas Question Outcome R = (Question → MIPRE.LIDT.Co.Measurement Outcome R)

@[reducible, inline]

abbrev MIPRE.LIDT.Co.IdxProjSubMeas (Question : Type u_1) (Outcome : Type u_2) (R : Type u_3) [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] : Type (max (max u_1 u_3) u_2)

Question-indexed family of projective submeasurements.

Equations

• MIPRE.LIDT.Co.IdxProjSubMeas Question Outcome R = (Question → MIPRE.LIDT.Co.ProjSubMeas Outcome R)

@[reducible, inline]

abbrev MIPRE.LIDT.Co.IdxProjMeas (Question : Type u_1) (Outcome : Type u_2) (R : Type u_3) [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] : Type (max (max u_1 u_3) u_2)

Question-indexed family of projective measurements.

Equations

• MIPRE.LIDT.Co.IdxProjMeas Question Outcome R = (Question → MIPRE.LIDT.Co.ProjMeas Outcome R)

def MIPRE.LIDT.Co.IdxMeas.toIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} {R : Type u_3} [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] (A : IdxMeas Question Outcome R) : IdxSubMeas Question Outcome R

Forget completeness from an indexed measurement family.

Equations

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

def MIPRE.LIDT.Co.IdxProjSubMeas.toIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} {R : Type u_3} [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] (A : IdxProjSubMeas Question Outcome R) : IdxSubMeas Question Outcome R

Forget projectivity from an indexed projective submeasurement family.

Equations

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

def MIPRE.LIDT.Co.IdxProjMeas.toIdxMeas {Question : Type u_1} {Outcome : Type u_2} {R : Type u_3} [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] (A : IdxProjMeas Question Outcome R) : IdxMeas Question Outcome R

Forget projectivity from an indexed projective measurement family.

Equations

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

def MIPRE.LIDT.Co.IdxProjMeas.toIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} {R : Type u_3} [Fintype Outcome] [Ring R] [StarRing R] [PartialOrder R] (A : IdxProjMeas Question Outcome R) : IdxSubMeas Question Outcome R

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

Equations

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

Postprocessing and transport

noncomputable def MIPRE.LIDT.Co.SubMeas.transport {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : SubMeas α R) : SubMeas β R

Transport a submeasurement along an equivalence of outcome types.

Equations

• MIPRE.LIDT.Co.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 MIPRE.LIDT.Co.SubMeas.transport_outcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : SubMeas α R) (b : β) : (transport e A).outcome b = A.outcome (e.symm b)

The outcome operator of the transport at b is the original one at e.symm b.

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.transport_total {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : SubMeas α R) : (transport e A).total = A.total

Transport keeps the total operator.

noncomputable def MIPRE.LIDT.Co.Measurement.transport {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : Measurement α R) : Measurement β R

Transport a measurement along an equivalence of outcome types.

Equations

• MIPRE.LIDT.Co.Measurement.transport e A = { toSubMeas := MIPRE.LIDT.Co.SubMeas.transport e A.toSubMeas, total_eq_one := ⋯ }

noncomputable def MIPRE.LIDT.Co.ProjSubMeas.transport {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : ProjSubMeas α R) : ProjSubMeas β R

Transport a projective submeasurement along an equivalence of outcome types.

Equations

• MIPRE.LIDT.Co.ProjSubMeas.transport e A = { toSubMeas := MIPRE.LIDT.Co.SubMeas.transport e A.toSubMeas, proj := ⋯ }

noncomputable def MIPRE.LIDT.Co.ProjMeas.transport {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : ProjMeas α R) : ProjMeas β R

Transport a projective measurement along an equivalence of outcome types.

Equations

• MIPRE.LIDT.Co.ProjMeas.transport e A = { toMeasurement := MIPRE.LIDT.Co.Measurement.transport e A.toMeasurement, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.ProjMeas.transport_toSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (e : α ≃ β) (A : ProjMeas α R) : (transport e A).toSubMeas = SubMeas.transport e A.toSubMeas

The transport of a projective measurement, as a submeasurement, is the transport of its submeasurement.

def MIPRE.LIDT.Co.constSubMeasFamily {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} [Fintype α] (A : SubMeas α R) : IdxSubMeas Unit α R

Constant indexed family taking the same submeasurement on every question.

Equations

• MIPRE.LIDT.Co.constSubMeasFamily A x✝ = A

noncomputable def MIPRE.LIDT.Co.postprocess {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α R) (f : α → β) : SubMeas β R

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

• MIPRE.LIDT.Co.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 MIPRE.LIDT.Co.SubMeas.postprocess_outcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] (A : SubMeas α R) (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 MIPRE.LIDT.Co.SubMeas.postprocess_id {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} [Fintype α] (A : SubMeas α R) : (postprocess A fun (a : α) => a) = A

Postprocessing a submeasurement by the identity readout leaves it unchanged.

theorem MIPRE.LIDT.Co.SubMeas.postprocess_transport {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] (e : α ≃ β) (A : SubMeas α R) (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 MIPRE.LIDT.Co.SubMeas.postprocess_transport_equiv {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] (eα : α ≃ β) (eγ : γ ≃ δ) (A : SubMeas α R) (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 MIPRE.LIDT.Co.SubMeas.postprocess_comp {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] (A : SubMeas α R) (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 MIPRE.LIDT.Co.completeSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} [Fintype α] (A : SubMeas α R) : Measurement (Option α) R

Complete a submeasurement by adjoining a distinguished failure outcome.

Equations

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

@[simp]

theorem MIPRE.LIDT.Co.ProjMeas.transport_trivialDistinguishedOutcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} [Fintype α] (e : α ≃ α) (a₀ : α) : transport e (trivialDistinguishedOutcome a₀) = trivialDistinguishedOutcome (e a₀)

Transporting the trivial measurement at a₀ along e gives the trivial measurement at e a₀.

theorem MIPRE.LIDT.Co.ProjSubMeas.postprocess_outcome_proj {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P : ProjSubMeas α R) (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 MIPRE.LIDT.Co.ProjMeas.postprocess {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : ProjMeas α R) (f : α → β) : ProjMeas β R

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 := MIPRE.LIDT.Co.postprocess A.toSubMeas f; { toSubMeas := __SubMeas, total_eq_one := ⋯ }, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.ProjMeas.postprocess_toSubMeas {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : ProjMeas α R) (f : α → β) : (A.postprocess f).toSubMeas = Co.postprocess A.toSubMeas f

The postprocessed projective measurement, as a submeasurement, is the postprocessed submeasurement.

theorem MIPRE.LIDT.Co.ProjMeas.postprocess_outcome_commute {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] (P : ProjMeas α R) (f : α → β) (g : α → γ) (b : β) (c : γ) : (Co.postprocess P.toSubMeas f).outcome b * (Co.postprocess P.toSubMeas g).outcome c = (Co.postprocess P.toSubMeas g).outcome c * (Co.postprocess P.toSubMeas f).outcome b

Postprocessed outcomes from the same ProjMeas commute.

Averages of indexed families

noncomputable def MIPRE.LIDT.Co.averageIdxSubMeas {Question : Type u_1} {Outcome : Type u_2} [Fintype Outcome] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [Module ℝ R] [IsOrderedAddMonoid R] [PosSMulMono ℝ R] [SMulPosMono ℝ R] [ZeroLEOneClass R] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome R) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : SubMeas Outcome R

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

noncomputable def MIPRE.LIDT.Co.SymModel.mkLeftPlacedSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : SubMeas α (K →L[ℂ] K)

Place a submeasurement on the first factor: each outcome A_a becomes S.L A_a (the vendored A_a ⊗ 1).

Equations

• S.mkLeftPlacedSubMeas A = MIPRE.LIDT.Co.SubMeas.map S.L A

noncomputable def MIPRE.LIDT.Co.SymModel.mkRightPlacedSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : SubMeas α (K →L[ℂ] K)

Place a submeasurement on the second factor: each outcome A_a becomes S.R A_a (the vendored 1 ⊗ A_a).

Equations

• S.mkRightPlacedSubMeas A = MIPRE.LIDT.Co.SubMeas.map S.R A

@[simp]

theorem MIPRE.LIDT.Co.SymModel.mkLeftPlacedSubMeas_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) (a : α) : (S.mkLeftPlacedSubMeas A).outcome a = S.L (A.outcome a)

Helper-level projection equation for left-placed outcomes.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.mkLeftPlacedSubMeas_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : (S.mkLeftPlacedSubMeas A).total = S.L A.total

Helper-level projection equation for left-placed totals.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.mkRightPlacedSubMeas_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) (a : α) : (S.mkRightPlacedSubMeas A).outcome a = S.R (A.outcome a)

Helper-level projection equation for right-placed outcomes.

@[simp]

theorem MIPRE.LIDT.Co.SymModel.mkRightPlacedSubMeas_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : (S.mkRightPlacedSubMeas A).total = S.R A.total

Helper-level projection equation for right-placed totals.

Square bipartite lifts

noncomputable def MIPRE.LIDT.Co.SubMeas.liftLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) : SubMeas α (K →L[ℂ] K)

Lift a submeasurement to the first factor. Each outcome operator A_a : 𝔓 becomes S.L A_a (the vendored A_a ⊗ I).

Equations

• MIPRE.LIDT.Co.SubMeas.liftLeft S A = S.mkLeftPlacedSubMeas A

noncomputable def MIPRE.LIDT.Co.IdxSubMeas.liftLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (A : IdxSubMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

Lift an indexed submeasurement family to the first factor.

Equations

• MIPRE.LIDT.Co.IdxSubMeas.liftLeft S A q = S.mkLeftPlacedSubMeas (A q)

noncomputable def MIPRE.LIDT.Co.ProjSubMeas.liftLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (A : ProjSubMeas α 𝔓) : ProjSubMeas α (K →L[ℂ] K)

Lift a projective submeasurement to the first factor.

Equations

• MIPRE.LIDT.Co.ProjSubMeas.liftLeft S A = { toSubMeas := MIPRE.LIDT.Co.SubMeas.liftLeft S A.toSubMeas, proj := ⋯ }

noncomputable def MIPRE.LIDT.Co.SubMeas.liftRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) : SubMeas α (K →L[ℂ] K)

Lift a submeasurement to the second factor. Each outcome operator A_a : 𝔓 becomes S.R A_a (the vendored I ⊗ A_a).

Equations

• MIPRE.LIDT.Co.SubMeas.liftRight S A = S.mkRightPlacedSubMeas A

noncomputable def MIPRE.LIDT.Co.IdxSubMeas.liftRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (A : IdxSubMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

Lift an indexed submeasurement family to the second factor.

Equations

• MIPRE.LIDT.Co.IdxSubMeas.liftRight S A q = S.mkRightPlacedSubMeas (A q)

General bipartite placement

noncomputable def MIPRE.LIDT.Co.SymModel.leftPlacedSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : SubMeas α (K →L[ℂ] K)

Place a submeasurement on the first factor.

Equations

• S.leftPlacedSubMeas A = S.mkLeftPlacedSubMeas A

@[simp]

theorem MIPRE.LIDT.Co.SymModel.leftPlacedSubMeas_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) (a : α) : (S.leftPlacedSubMeas A).outcome a = S.L (A.outcome a)

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

@[simp]

theorem MIPRE.LIDT.Co.SymModel.leftPlacedSubMeas_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : (S.leftPlacedSubMeas A).total = S.L A.total

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

noncomputable def MIPRE.LIDT.Co.SymModel.rightPlacedSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : SubMeas α (K →L[ℂ] K)

Place a submeasurement on the second factor.

Equations

• S.rightPlacedSubMeas A = S.mkRightPlacedSubMeas A

@[simp]

theorem MIPRE.LIDT.Co.SymModel.rightPlacedSubMeas_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) (a : α) : (S.rightPlacedSubMeas A).outcome a = S.R (A.outcome a)

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

@[simp]

theorem MIPRE.LIDT.Co.SymModel.rightPlacedSubMeas_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : (S.rightPlacedSubMeas A).total = S.R A.total

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

noncomputable def MIPRE.LIDT.Co.IdxSubMeas.placeLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (A : IdxSubMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

Lift an indexed submeasurement family to the first factor (general bipartite placement).

Equations

• MIPRE.LIDT.Co.IdxSubMeas.placeLeft S A q = S.mkLeftPlacedSubMeas (A q)

noncomputable def MIPRE.LIDT.Co.IdxSubMeas.placeRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (A : IdxSubMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

Lift an indexed submeasurement family to the second factor (general bipartite placement).

Equations

• MIPRE.LIDT.Co.IdxSubMeas.placeRight S A q = S.mkRightPlacedSubMeas (A q)