Section 11 commutativity: the point-swap bound for the evaluated-slice paper chain

The right-register point-swap estimate used in the paper-faithful scalar chain for lem:comm-data-processed-g: the counterpart of Commutativity/ScalarApproximation/PaperChainBasic/PointSwap.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

Both lemmas drop the vendored hypothesis hnorm : strategy.state.IsNormalized, a theorem of the model, so the argument order is params strategy gamma hcomm C hC and params strategy eps delta gamma hgood C hC. The family C is a family of joint operators K →L[ℂ] K, and hC is stated with star. The swap of the point product from the right to the left register is Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv, which applies the model's S.ev_L_eq_ev_R in place of the vendored strategy.permInvState.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseFour_pointSwap_right_bound_of_commutativityPoints {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (gamma : ℝ) (hcomm : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params.next)) (CommutativityPoints.pointMeasurementProductLeft params.next strategy) (CommutativityPoints.pointMeasurementProductRight params.next strategy) (MIPStarRE.LDT.CommutativityPoints.commutativityPointsError params.next gamma)) (C : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params → MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params → K →L[ℂ] K) (hC : ∀ (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params), ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, C q ab * star (C q ab) ≤ 1) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have inserted := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, strategy.state.ev (C q ab * strategy.state.R ((evaluatedSlicePointMeas params strategy q.2).outcome ab.2 * (evaluatedSlicePointMeas params strategy q.1).outcome ab.1)); have swapped := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, strategy.state.ev (C q ab * strategy.state.R ((evaluatedSlicePointMeas params strategy q.1).outcome ab.1 * (evaluatedSlicePointMeas params strategy q.2).outcome ab.2)); |MIPStarRE.LDT.avgOver 𝒟 inserted - MIPStarRE.LDT.avgOver 𝒟 swapped| ≤ 6 * √(gamma * ↑(params.m + 1))

The right-register point swap, from the point commutativity of thm:commutativity-points: for a family C with ∑_{ab} C_{ab} C_{ab}^* ≤ 1 at every question, swapping the order of the two point measurements placed on the right register moves the averaged expectation by at most 6 √(γ (m + 1)).

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseFour_pointSwap_right_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) (C : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params → MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params → K →L[ℂ] K) (hC : ∀ (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params), ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, C q ab * star (C q ab) ≤ 1) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have inserted := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, strategy.state.ev (C q ab * strategy.state.R ((evaluatedSlicePointMeas params strategy q.2).outcome ab.2 * (evaluatedSlicePointMeas params strategy q.1).outcome ab.1)); have swapped := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, strategy.state.ev (C q ab * strategy.state.R ((evaluatedSlicePointMeas params strategy q.1).outcome ab.1 * (evaluatedSlicePointMeas params strategy q.2).outcome ab.2)); |MIPStarRE.LDT.avgOver 𝒟 inserted - MIPStarRE.LDT.avgOver 𝒟 swapped| ≤ 6 * √(gamma * ↑(params.m + 1))

The right-register point swap for a good strategy: thm:commutativity-points supplies the point commutativity of evaluatedSlice_phaseFour_pointSwap_right_bound_of_commutativityPoints.