Phase-seven reverse insertion for the evaluated-slice paper chain #
This file proves the second reverse eq:add-an-a bound used after the
paper line-87 phase-five removal.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseSeven_second_reverse_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 phase6FirstRemoved := evaluatedSlicePhaseSixFirstRemoved params strategy family;
have phase7GonnaCite := evaluatedSlicePhaseSevenGonnaCite params strategy family;
|avgOver 𝒟 phase6FirstRemoved - avgOver 𝒟 phase7GonnaCite| ≤ 2 * √zeta
Paper lines 103--104: reverse the second eq:add-an-a insertion.