Section 12 pasting: complete-part reductions #
Complete-part aggregate commutation and scalar error bounds.
theorem
MIPStarRE.LDT.Pasting.completePartAggregateCommutation_as_total
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(gamma : Error)
(hcomm :
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params))
(switcherooAggregateLeft params family (completePartProjFamily params family))
(switcherooAggregateRight params family (completePartProjFamily params family)) gamma)
:
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (completePartTotalProductLeft params family)
(completePartTotalProductRight params family) gamma
When the left/right aggregate families are re-expressed using the completed one-outcome form, the aggregate commutation bound translates to the complete-part total-product commutation bound.
theorem
MIPStarRE.LDT.Pasting.firstSwitcherooError_le_eighth_stage
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta : zeta ≤ 1)
(hd_le_q : params.d ≤ params.q)
:
Variant of the first switcheroo scalar bound using the intermediate
eighthSum; shared with CommutingWithG/Complete.
theorem
MIPStarRE.LDT.Pasting.firstSwitcherooError_le_commutingWithGCompleteError
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(hgamma_nonneg : 0 ≤ gamma)
(hgamma : gamma ≤ 1)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta : zeta ≤ 1)
(hd_le_q : params.d ≤ params.q)
:
commutativitySwitcherooError zeta zeta (Commutativity.comMainError params gamma zeta) ≤ commutingWithGCompleteError params gamma zeta
Many sqrt/rpow manipulations for 12 * sqrt zeta + 4 * sqrt (ν_com) ≤ ν₂.
This shows that the first-switcheroo error (the commutativitySwitcherooError)
is bounded above by the complete-part commuting-with-G error.