Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Pasting.Sandwich.GHatSandwich

Section 12 — Sandwich constructions: GHat sandwich families #

Completed-slice sandwich families and restriction helpers.

source
theorem MIPStarRE.LDT.Pasting.binomialOperatorTerm_nonneg {ι : Type u} [Fintype ι] [DecidableEq ι] {G : Quantum.Op ι} (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 semidefinite.

source
theorem MIPStarRE.LDT.Pasting.bernoulliTailOperator_nonneg {ι : Type u} [Fintype ι] [DecidableEq ι] (k degree : ℕ) (G : Quantum.Op ι) (hG : 0 ≤ G) (hGle : G ≤ 1) :
0 ≤ bernoulliTailOperator k degree G

Positivity of the Bernoulli tail operator for a PSD contraction.

source
theorem MIPStarRE.LDT.Pasting.bernoulliTailOperator_le_one {ι : Type u} [Fintype ι] [DecidableEq ι] (k degree : ℕ) (G : Quantum.Op ι) (hG : 0 ≤ G) (hGle : G ≤ 1) :
bernoulliTailOperator k degree G ≤ 1

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

source
noncomputable def MIPStarRE.LDT.Pasting.gHatSandwichFamily {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) :
IdxSubMeas (PointTuple params k) (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 MIPStarRE.LDT.Pasting.restrictSubMeas {ι : Type u} [Fintype ι] [DecidableEq ι] {α : Type u_1} [Fintype α] (A : SubMeas α ι) (p : α → Prop) [DecidablePred p] :
    SubMeas α ι

    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 MIPStarRE.LDT.Pasting.restrictSubMeas_total_le_total {ι : Type u} [Fintype ι] [DecidableEq ι] {α : Type u_1} [Fintype α] (A : SubMeas α ι) (p : α → Prop) [DecidablePred p] :
      (restrictSubMeas A p).total ≤ A.total

      Restricting a submeasurement can only decrease its total operator.

      source
      noncomputable def MIPStarRE.LDT.Pasting.interpolationEligibleSandwichFamily {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) :
      IdxSubMeas (PointTuple params k) (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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPStarRE.LDT.Pasting.gHatHalfSandwichLeft {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) :
        IdxOpFamily (PointTuple params k) (GHatTupleOutcome params k) (ι × ι)

        Concrete family for the half-sandwich product of k completed slices.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPStarRE.LDT.Pasting.gHatHalfSandwichRight {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) :
          IdxOpFamily (PointTuple params k) (GHatTupleOutcome params k) (ι × ι)

          Concrete family for the cyclically permuted half-sandwich product.

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