Phase-six reverse insertion for the evaluated-slice paper chain #
This file proves the first reverse eq:add-an-a bound used after the
paper line-87 phase-five removal.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseSix_first_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_fst :
SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.1)
(fun (q : EvaluatedSliceQuestion params) =>
Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy)
q.1)
(4 * zeta))
:
have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params);
have phase5PaperRemoved := evaluatedSlicePhaseFivePaperRemoved params strategy family;
have phase6FirstRemoved := evaluatedSlicePhaseSixFirstRemoved params strategy family;
|avgOver 𝒟 phase5PaperRemoved - avgOver 𝒟 phase6FirstRemoved| ≤ 2 * √zeta
Paper lines 99--102: reverse the first eq:add-an-a insertion after eq:gcom10.