Section 12 — Sandwich constructions: `GHat` sandwich families #

Completed-slice sandwich families and restriction helpers: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Sandwich/GHatSandwich.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The positivity and boundedness of the Bernoulli tail operator read no state, so they hold in any C*-algebra with its order (𝔓 and K →L[ℂ] K alike), through CStarAlgebra.pow_nonneg and Commute.mul_nonneg in place of the vendored Matrix.PosSemidef arguments; the restriction of a submeasurement holds in any ordered ⋆-ring. The sandwiched family \widehat G^{x_1}_{g_1} \cdots \widehat G^{x_k}_{g_k} \cdots \widehat G^{x_1}_{g_1} is a local family in 𝔓, and the two half-sandwich families take the symmetric model S : SymModel 𝔓 K as their first explicit argument, in place of the vendored named carrier (ιB := ι), and place by OpFamily.leftPlacedOpFamily S.

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/ld-pasting.tex

source

theorem MIPRE.LIDT.Co.Pasting.binomialOperatorTerm_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {G : A} (n r : ℕ) (hG : 0 ≤ G) (hGle : G ≤ 1) :

0 ≤ ↑(n.choose r) • (G ^ r * (1 - G) ^ (n - r))

Each binomial term in the Bernoulli tail operator is positive.

source

theorem MIPRE.LIDT.Co.Pasting.bernoulliTailOperator_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (k degree : ℕ) (G : A) (hG : 0 ≤ G) (hGle : G ≤ 1) :

0 ≤ bernoulliTailOperator k degree G

Positivity of the Bernoulli tail operator for a positive contraction.

source

theorem MIPRE.LIDT.Co.Pasting.bernoulliTailOperator_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (k degree : ℕ) (G : A) (hG : 0 ≤ G) (hGle : G ≤ 1) :

bernoulliTailOperator k degree G ≤ 1

The Bernoulli tail operator is bounded by the identity for a positive contraction.

source

noncomputable def MIPRE.LIDT.Co.Pasting.gHatSandwichFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) :

IdxSubMeas (MIPStarRE.LDT.PointTuple params k) (MIPStarRE.LDT.Pasting.GHatTupleOutcome params k) 𝔓

Concrete family for the full sandwich \widehat G^{x_1}_{g_1} \cdots \widehat G^{x_k}_{g_k} \cdots \widehat G^{x_1}_{g_1}.

Equations

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

Instances For

source

noncomputable def MIPRE.LIDT.Co.Pasting.restrictSubMeas {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_4} [Fintype α] (A : SubMeas α R) (p : α → Prop) [DecidablePred p] :

SubMeas α R

Restrict a submeasurement to the outcomes satisfying p, dropping all other mass from the total operator.

Equations

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

Instances For

source

theorem MIPRE.LIDT.Co.Pasting.restrictSubMeas_total_le_total {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_4} [Fintype α] (A : SubMeas α R) (p : α → Prop) [DecidablePred p] :

(restrictSubMeas A p).total ≤ A.total

Restricting a submeasurement can only decrease its total operator.

source

noncomputable def MIPRE.LIDT.Co.Pasting.interpolationEligibleSandwichFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) :

IdxSubMeas (MIPStarRE.LDT.PointTuple params k) (MIPStarRE.LDT.Pasting.GHatTupleOutcome params k) 𝔓

Restrict the sandwiched completed-slice family to tuples with support of size at least d + 1, matching the |τ| ≥ d+1 filter in the paper before interpolation.

Equations