Section 12 pasting: switcheroo aggregate terms #
The remaining switcheroo aggregate terms and split formulas.
noncomputable def
MIPStarRE.LDT.Pasting.completePartProjFamily
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
:
IdxProjSubMeas (SliceQuestion params) Unit ι
The one-outcome projective family whose sole effect is the complete slice part G^x.
Equations
- MIPStarRE.LDT.Pasting.completePartProjFamily params family x = { toSubMeas := MIPStarRE.LDT.Pasting.completePartSubMeas params family x, proj := ⋯ }
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateSecondTerm
{ι : 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 ι)
:
The second positive term in the switcheroo expansion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateThirdTerm
{ι : 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 ι)
:
The third (negative) term in the switcheroo expansion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm
{ι : 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 ι)
:
The fourth (negative) term in the switcheroo expansion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateThirdTerm_eq_fourthTerm
{ι : 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 ι)
:
switcherooAggregateThirdTerm params ψbi family M = switcherooAggregateFourthTerm params ψbi family M
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_eq_split
{ι : 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 ι)
:
switcherooAggregateFourthTerm params ψbi family M = avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) =>
∑ go : Polynomial params × Outcome,
ev ψbi
(leftTensor
((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))
Split the fourth switcheroo term by inserting the complete-part projector
resolution G = ∑_g G_g.