Section 12 pasting: switcheroo scalar expressions #
Named scalar expressions for the switcheroo contraction chain.
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateLeftFrontScalar
{ι : 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 post-second-√ζ left-front expression in the paper's cross-term chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateFirstSplitScalar
{ι : 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 split-by-g expression that collapses back to the first positive term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateOnceCommutedScalar
{ι : 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 post-first-√χ scalar expression in the fourth-term chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_close_once_commuted_scalar
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(hnorm : ψbi.IsNormalized)
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(chi : Error)
(hcomm :
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (switcherooPointProductLeft params family M)
(switcherooPointProductRight params family M) chi)
:
|switcherooAggregateFourthTerm params ψbi family M - switcherooAggregateOnceCommutedScalar params ψbi family M| ≤ √chi
Restate the first sqrt chi step using the named scalar expression.
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateMixedScalar
{ι : 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 post-first-√ζ mixed tensor scalar expression in the fourth-term chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_mixed_close_left_front_scalar
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(hnorm : ψbi.IsNormalized)
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(zeta : Error)
(hselfG : GCompleteSelfConsistencyStatement params ψbi family zeta)
:
|(avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) =>
∑ g : Polynomial params,
∑ o : Outcome,
ev ψbi
(leftTensor ((family.meas q.1).outcome g) * leftTensor
((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o))) - avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) =>
∑ g : Polynomial params,
∑ o : Outcome,
ev ψbi
(rightTensor ((family.meas q.1).outcome g) * leftTensor
((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o))| ≤ √zeta
Restate the second sqrt zeta step using the named left-front scalar
expression.