Section 12 pasting: switcheroo expansion #
Expansion identities and the left-front contraction bound.
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateLeftFront_contraction
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(q : SlicePairQuestion params)
:
∑ go : Polynomial params × Outcome,
(∑ _u : Unit, leftTensor ((family.meas q.1).outcome go.1 * (M q.2).outcome go.2)).conjTranspose * ∑ _u : Unit, leftTensor ((family.meas q.1).outcome go.1 * (M q.2).outcome go.2) ≤ 1
Contraction witness for the final sqrt chi left-front overlap step.
theorem
MIPStarRE.LDT.Pasting.switcherooPointProductLeft_self_eq_firstSplit_point
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(q : SlicePairQuestion params)
(go : Polynomial params × Outcome)
:
ev ψbi
(Matrix.conjTranspose ((switcherooPointProductLeft params family M q).outcome go) * (switcherooPointProductLeft params family M q).outcome go) = ev ψbi (leftTensor ((M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))
Normalize the pointwise self-product in the final switcheroo left-front
step to the split-by-g scalar.
theorem
MIPStarRE.LDT.Pasting.switcherooPointProductRightLeft_eq_leftFront_point
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(q : SlicePairQuestion params)
(go : Polynomial params × Outcome)
:
ev ψbi
(Matrix.conjTranspose ((switcherooPointProductRight params family M q).outcome go) * (switcherooPointProductLeft params family M q).outcome go) = ev ψbi
(leftTensor
((family.meas q.1).outcome go.1 * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))
Normalize the pointwise mixed product in the final switcheroo left-front step into the left-front scalar form.
theorem
MIPStarRE.LDT.Pasting.switcherooAggregate_qSDDOp_expand_avg
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
:
(avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) =>
qSDDOp ψbi (switcherooAggregateLeft params family M q) (switcherooAggregateRight params family M q)) = switcherooAggregateFirstTerm params ψbi family M + switcherooAggregateSecondTerm params ψbi family M - switcherooAggregateThirdTerm params ψbi family M - switcherooAggregateFourthTerm params ψbi family M
Average the single-question four-term qSDDOp expansion over the
slice-pair distribution.