Point-swap bound for the evaluated-slice paper chain #
This file contains the right-register point-swap estimate used in the
paper-faithful scalar chain for lem:comm-data-processed-g.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseFour_pointSwap_right_bound_of_commutativityPoints
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(gamma : Error)
(hnorm : strategy.state.IsNormalized)
(hcomm :
SDDOpRel strategy.state (uniformDistribution (GlobalVariance.PointPairQuestion params.next))
(CommutativityPoints.pointMeasurementProductLeft params.next strategy)
(CommutativityPoints.pointMeasurementProductRight params.next strategy)
(CommutativityPoints.commutativityPointsError params.next gamma))
(C : EvaluatedSliceQuestion params → EvaluatedSliceOutcome params → Quantum.Op (ι × ι))
(hC :
∀ (q : EvaluatedSliceQuestion params),
∑ ab : EvaluatedSliceOutcome params, C q ab * Matrix.conjTranspose (C q ab) ≤ 1)
:
have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params);
have inserted := fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params,
ev strategy.state
(C q ab * rightTensor
((evaluatedSlicePointMeas params strategy q.2).outcome ab.2 * (evaluatedSlicePointMeas params strategy q.1).outcome ab.1));
have swapped := fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params,
ev strategy.state
(C q ab * rightTensor
((evaluatedSlicePointMeas params strategy q.1).outcome ab.1 * (evaluatedSlicePointMeas params strategy q.2).outcome ab.2));
|avgOver 𝒟 inserted - avgOver 𝒟 swapped| ≤ 6 * √(gamma * ↑(params.m + 1))
theorem
MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseFour_pointSwap_right_bound
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma : Error)
(hnorm : strategy.state.IsNormalized)
(hgood : strategy.IsGood eps delta gamma)
(C : EvaluatedSliceQuestion params → EvaluatedSliceOutcome params → Quantum.Op (ι × ι))
(hC :
∀ (q : EvaluatedSliceQuestion params),
∑ ab : EvaluatedSliceOutcome params, C q ab * Matrix.conjTranspose (C q ab) ≤ 1)
:
have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params);
have inserted := fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params,
ev strategy.state
(C q ab * rightTensor
((evaluatedSlicePointMeas params strategy q.2).outcome ab.2 * (evaluatedSlicePointMeas params strategy q.1).outcome ab.1));
have swapped := fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params,
ev strategy.state
(C q ab * rightTensor
((evaluatedSlicePointMeas params strategy q.1).outcome ab.1 * (evaluatedSlicePointMeas params strategy q.2).outcome ab.2));
|avgOver 𝒟 inserted - avgOver 𝒟 swapped| ≤ 6 * √(gamma * ↑(params.m + 1))