Section 12 pasting: switcheroo centers #
Switcheroo center terms and their sandwich rewrites.
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateTarget
{ι : 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 common comparison scalar ⟨ψ, G ⊗ M ψ⟩ from the switcheroo proof.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.switcherooAggregateFirstTerm
{ι : 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 first positive term in the switcheroo expansion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateFirstTerm_eq_leftSandwich
{ι : 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 ι)
:
switcherooAggregateFirstTerm params ψbi family M = avgOver (uniformDistribution (SliceQuestion params)) fun (x : SliceQuestion params) =>
Preliminaries.leftSandwichExpectation ψbi (uniformDistribution (SliceQuestion params)) M
(completePartSubMeas params family x).total
Rewrite the first positive switcheroo term as a left-sandwich average.
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateTarget_eq_middleSandwich
{ι : 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 ι)
:
switcherooAggregateTarget params ψbi family M = avgOver (uniformDistribution (SliceQuestion params)) fun (x : SliceQuestion params) =>
Preliminaries.middleSandwichExpectation ψbi (uniformDistribution (SliceQuestion params)) M
(completePartSubMeas params family x).total
Rewrite the G ⊗ M switcheroo center as a middle-sandwich average.
theorem
MIPStarRE.LDT.Pasting.switcheroo_first_term_close
{ι : 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 ι)
(omega : Error)
(hselfM :
SDDRel ψbi (uniformDistribution (SliceQuestion params)) (switcherooSelfConsistencyLeft params M)
(switcherooSelfConsistencyRight params M) omega)
:
have firstTerm :=
avgOver (uniformDistribution (SliceQuestion params)) fun (x : SliceQuestion params) =>
Preliminaries.leftSandwichExpectation ψbi (uniformDistribution (SliceQuestion params)) M
(completePartSubMeas params family x).total;
have commonTerm :=
avgOver (uniformDistribution (SliceQuestion params)) fun (x : SliceQuestion params) =>
Preliminaries.middleSandwichExpectation ψbi (uniformDistribution (SliceQuestion params)) M
(completePartSubMeas params family x).total;
|firstTerm - commonTerm| ≤ 2 * √omega
The first positive switcheroo term is close to the G ⊗ M center via the
self-consistency of M.