Section 11 commutativity: the phase-1 evaluated-slice insertion bound

Closeness-of-inner-product side conditions for inserting Bob's measurement into the first evaluated-slice step of the paper proof. The normalization lemmas remain formulated at the level needed by the evaluated-slice transport arguments, but the public bound in this file is now the phase-1 insertion estimate.

References

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePointMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) : IdxMeas (Point params.next) (Fq params) ι

View the params.next point measurement with the outcome type rewritten as Fq params.

Equations

• MIPStarRE.LDT.Commutativity.evaluatedSlicePointMeas params strategy u = (strategy.pointMeasurement u).toMeasurement

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseOne_insert_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (family : IdxPolyFamily params ι) (hcombined_snd : SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) (fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.2) (fun (q : EvaluatedSliceQuestion params) => Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2) (4 * zeta)) : have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params); have inserted := fun (q : EvaluatedSliceQuestion params) => ∑ b : Fq params, ∑ a : Fq params, ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a) * (Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2).outcome b); |(avgOver 𝒟 fun (q : EvaluatedSliceQuestion params) => ∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab) - avgOver 𝒟 inserted| ≤ 2 * √zeta

Phase-1 insertion step for evaluatedSlice_scalar_chain_bound.

This is the eq:gcom8 -> eq:apply-add-an-a-once comparison: transport the pointwise consSubMeas control to the second coordinate of an evaluated-slice question, then apply closenessOfIP with the left-sandwich family G_a^{u,x} G_b^{v,y} G_a^{u,x}. The inserted term is kept in the explicit G^y \otimes A_b^{v,y} form coming from totalSandwichFamily.