Section 12 — Sandwich constructions: switcheroo families

Switcheroo, complete-part, and half-product operator families.

def MIPStarRE.LDT.Pasting.switcherooSelfConsistencyLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (M : IdxProjSubMeas (Fq params) Outcome ι) : IdxSubMeas (SliceQuestion params) Outcome (ι × ι)

Left tensor-placement for the auxiliary family M^x_o.

Equations

• MIPStarRE.LDT.Pasting.switcherooSelfConsistencyLeft params M x = MIPStarRE.LDT.leftPlacedSubMeas (M x).toSubMeas

def MIPStarRE.LDT.Pasting.switcherooSelfConsistencyRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (M : IdxProjSubMeas (Fq params) Outcome ι) : IdxSubMeas (SliceQuestion params) Outcome (ι × ι)

Right tensor-placement for the auxiliary family M^x_o.

Equations

• MIPStarRE.LDT.Pasting.switcherooSelfConsistencyRight params M x = MIPStarRE.LDT.rightPlacedSubMeas (M x).toSubMeas

noncomputable def MIPStarRE.LDT.Pasting.switcherooPointProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) : IdxOpFamily (SlicePairQuestion params) (Polynomial params × Outcome) (ι × ι)

Concrete hypothesis family for G^x_g M^y_o.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.switcherooPointProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) : IdxOpFamily (SlicePairQuestion params) (Polynomial params × Outcome) (ι × ι)

Concrete hypothesis family for M^y_o G^x_g on the Polynomial params × Outcome outcome type.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.switcherooAggregateLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) : IdxOpFamily (SlicePairQuestion params) Outcome (ι × ι)

Concrete aggregate family for G^x M^y_o.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.switcherooAggregateRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) : IdxOpFamily (SlicePairQuestion params) Outcome (ι × ι)

Concrete aggregate family for M^y_o G^x.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.completePartPointProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) (Polynomial params) (ι × ι)

Concrete family for G^x_g G^y.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.completePartPointProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) (Polynomial params) (ι × ι)

Concrete family for G^y G^x_g.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.completePartTotalProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) Unit (ι × ι)

Concrete family for G^x G^y.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.completePartTotalProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) Unit (ι × ι)

Concrete family for G^y G^x.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.incompletePartPointProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) (Polynomial params) (ι × ι)

Concrete family for G^x_g G^y_⊥.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.incompletePartPointProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) (Polynomial params) (ι × ι)

Concrete family for G^y_⊥ G^x_g.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.incompletePartTotalProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) Unit (ι × ι)

Concrete family for G^x_⊥ G^y_⊥.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.incompletePartTotalProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) Unit (ι × ι)

Concrete family for G^y_⊥ G^x_⊥.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.gHatSelfConsistencyLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (SliceQuestion params) (GHatOutcome params) (ι × ι)

Left tensor-placement for \widehat G^x_g.

Equations

• MIPStarRE.LDT.Pasting.gHatSelfConsistencyLeftFamily params family x = MIPStarRE.LDT.leftPlacedSubMeas (MIPStarRE.LDT.Pasting.gHatIdxMeas params family x).toSubMeas

noncomputable def MIPStarRE.LDT.Pasting.gHatSelfConsistencyRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (SliceQuestion params) (GHatOutcome params) (ι × ι)

Right tensor-placement for \widehat G^x_g.

Equations

• MIPStarRE.LDT.Pasting.gHatSelfConsistencyRightFamily params family x = MIPStarRE.LDT.rightPlacedSubMeas (MIPStarRE.LDT.Pasting.gHatIdxMeas params family x).toSubMeas

noncomputable def MIPStarRE.LDT.Pasting.gHatPairProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) (GHatOutcome params × GHatOutcome params) (ι × ι)

Concrete family for the pairwise product \widehat G^x_g \widehat G^y_h.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.gHatPairProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxOpFamily (SlicePairQuestion params) (GHatOutcome params × GHatOutcome params) (ι × ι)

Concrete family for the reversed pairwise product \widehat G^y_h \widehat G^x_g.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.gHatHalfProductOutcomeOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) : PointTuple params k → GHatTupleOutcome params k → Quantum.Op ι

The ordered half-product \widehat G^{x_1}_{g_1} \cdots \widehat G^{x_k}_{g_k}.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.gHatHalfProductOutcomeOperator params family 0 _xs _gs = 1

noncomputable def MIPStarRE.LDT.Pasting.gHatHalfProductTotalOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) : PointTuple params k → Quantum.Op ι

The total half-product \sum_{g_1,\dots,g_k} \widehat G^{x_1}_{g_1} \cdots \widehat G^{x_k}_{g_k}.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.gHatHalfProductTotalOperator params family 0 _xs = 1

noncomputable def MIPStarRE.LDT.Pasting.gHatRotatedHalfProductOutcomeOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) : PointTuple params k → GHatTupleOutcome params k → Quantum.Op ι

The cyclically rotated half-product \widehat G^{x_2}_{g_2} \cdots \widehat G^{x_k}_{g_k} \widehat G^{x_1}_{g_1}.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.gHatRotatedHalfProductOutcomeOperator params family 0 _xs _gs = 1

noncomputable def MIPStarRE.LDT.Pasting.gHatRotatedHalfProductTotalOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) : PointTuple params k → Quantum.Op ι

The total cyclically rotated half-product.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.gHatRotatedHalfProductTotalOperator params family 0 _xs = 1

def MIPStarRE.LDT.Pasting.gHatTupleOutcomeConsEquiv' (params : Parameters) [FieldModel params.q] (k : ℕ) : GHatTupleOutcome params (k + 1) ≃ GHatOutcome params × GHatTupleOutcome params k

Splitting a nonempty completed-outcome tuple into its first outcome and tail.

Equations

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

theorem MIPStarRE.LDT.Pasting.gHatHalfProductTotalOperator_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (xs : PointTuple params k) : gHatHalfProductTotalOperator params family k xs = 1

The total operator of the ordered half-product is always the identity.

theorem MIPStarRE.LDT.Pasting.gHatHalfProduct_sum_eq_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (xs : PointTuple params k) : ∑ gs : GHatTupleOutcome params k, gHatHalfProductOutcomeOperator params family k xs gs = gHatHalfProductTotalOperator params family k xs

Summing the ordered half-product over all completed outcomes gives its total operator.