Raw operator families for the low individual degree test

This file introduces the notion of an indexed family of operators used in the paper without positivity or boundedness requirements. These are used for ≈_δ chains whose intermediate objects are arbitrary operator families rather than honest submeasurements: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/OpFamily.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The vendored families have their operators in the matrix algebra Op ι. Here a raw family has its operators in an arbitrary type R, with no structure at all (the postprocessing asks for an additive monoid to sum fibres in): local families take R = 𝔓, joint ones R = K →L[ℂ] K. A family is placed on a tensor factor by OpFamily.map along S.L or S.R, so (A.leftPlacedOpFamily S).outcome a = S.L (A.outcome a) holds by rfl; the placements take the symmetric model S as their first explicit argument, in place of the vendored named carriers (ιB := ιB), as SubMeas.liftLeft does in Co/Basic/SubMeasurementFamilies.lean.

New here

OpFamily.map (the image of a family under a map of operator types) and its projections map_outcome, map_total, and SubMeas.toOpFamily_map (forgetting commutes with map).

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/self_improvement.tex
• references/ldt-paper/commutativity-points.tex
• references/ldt-paper/commutativity-G.tex
• references/ldt-paper/ld-pasting.tex

structure MIPRE.LIDT.Co.OpFamily (α : Type u_1) (R : Type u_2) : Type (max u_1 u_2)

A raw operator family: outcome operators indexed by α, without positivity or bound requirements. This matches the paper's use of arbitrary operator families in ≈_δ chains.

• outcome : α → R
• total : R

def MIPRE.LIDT.Co.IdxOpFamily (Question : Type u_1) (Outcome : Type u_2) (R : Type u_3) : Type (max (max u_1 u_3) u_2)

Indexed raw operator family (question → outcome → operator).

Equations

• MIPRE.LIDT.Co.IdxOpFamily Question Outcome R = (Question → MIPRE.LIDT.Co.OpFamily Outcome R)

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

Forget the positivity and boundedness structure of a submeasurement.

Equations

• A.toOpFamily = { outcome := A.outcome, total := A.total }

@[instance_reducible]

instance MIPRE.LIDT.Co.instCoeSubMeasOpFamily {α : Type u_1} {R : Type u_2} [Fintype α] [Ring R] [StarRing R] [PartialOrder R] : Coe (SubMeas α R) (OpFamily α R)

A submeasurement is a raw operator family.

Equations

• MIPRE.LIDT.Co.instCoeSubMeasOpFamily = { coe := MIPRE.LIDT.Co.SubMeas.toOpFamily }

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

Forget the positivity and boundedness structure of an indexed submeasurement family.

Equations

• A.toIdxOpFamily q = (A q).toOpFamily

def MIPRE.LIDT.Co.OpFamily.map {α : Type u_1} {R : Type u_2} {T : Type u_3} (f : R → T) (A : OpFamily α R) : OpFamily α T

The image of a raw operator family under a map of operator types, applied to every outcome operator and to the total.

Equations

• MIPRE.LIDT.Co.OpFamily.map f A = { outcome := fun (a : α) => f (A.outcome a), total := f A.total }

@[simp]

theorem MIPRE.LIDT.Co.OpFamily.map_outcome {α : Type u_1} {R : Type u_2} {T : Type u_3} (f : R → T) (A : OpFamily α 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.OpFamily.map_total {α : Type u_1} {R : Type u_2} {T : Type u_3} (f : R → T) (A : OpFamily α R) : (map f A).total = f A.total

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

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

Place a raw operator family on the first tensor factor: each operator A_a becomes S.L A_a (the vendored A_a ⊗ 1).

Equations

• MIPRE.LIDT.Co.OpFamily.leftPlacedOpFamily S A = MIPRE.LIDT.Co.OpFamily.map (⇑S.L) A

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

Place a raw operator family on the second tensor factor: each operator A_a becomes S.R A_a (the vendored 1 ⊗ A_a).

Equations

• MIPRE.LIDT.Co.OpFamily.rightPlacedOpFamily S A = MIPRE.LIDT.Co.OpFamily.map (⇑S.R) A

noncomputable def MIPRE.LIDT.Co.OpFamily.postprocess {α : Type u_1} {β : Type u_2} {R : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid R] (A : OpFamily α R) (f : α → β) : OpFamily β R

Post-process the outcomes of a raw operator family.

Equations

• A.postprocess f = { outcome := fun (b : β) => ∑ a : α with f a = b, A.outcome a, total := A.total }

@[simp]

theorem MIPRE.LIDT.Co.SubMeas.toOpFamily_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) : (map f A).toOpFamily = OpFamily.map (⇑f) A.toOpFamily

Forgetting the submeasurement structure commutes with taking the image under a ⋆-homomorphism.

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

Lift an indexed raw operator family to the first tensor factor.

Equations

• MIPRE.LIDT.Co.IdxOpFamily.liftLeft S A q = MIPRE.LIDT.Co.OpFamily.leftPlacedOpFamily S (A q)