Tail endpoints for the evaluated-slice paper chain #
This file proves the two postprocessed self-consistency tail moves at the end of the paper-faithful scalar chain.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseEight_tail_bound
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(zeta : Error)
(hnorm : strategy.state.IsNormalized)
(family : IdxPolyFamily params ι)
(hpostSSC_snd :
SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.2)
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyRight params family q.2) zeta)
:
have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params);
have phase7GonnaCite := evaluatedSlicePhaseSevenGonnaCite params strategy family;
have phase8TailRight := evaluatedSlicePhaseEightTailRight params strategy family;
|avgOver 𝒟 phase7GonnaCite - avgOver 𝒟 phase8TailRight| ≤ √zeta
Paper line 117--118: move the second-coordinate factor to the right register.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseNine_tail_bound
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(zeta : Error)
(hnorm : strategy.state.IsNormalized)
(family : IdxPolyFamily params ι)
(hpostSSC_snd :
SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.2)
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyRight params family q.2) zeta)
:
have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params);
have phase8TailRight := evaluatedSlicePhaseEightTailRight params strategy family;
have avgBAB := fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceBABTerm params strategy family q ab;
|avgOver 𝒟 phase8TailRight - avgOver 𝒟 avgBAB| ≤ √zeta
Paper line 118--119: move the second-coordinate factor back to the left register.