Section 11 commutativity: evaluated-slice commutation consequences #
Downstream consequences of the evaluated-slice commutation estimate: pulling single-point evaluated-family self-consistency bounds up to evaluated-slice questions.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.evaluatedPointSelfConsistency_fst
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(zeta : Error)
(hssc :
SDDRel strategy.state (uniformDistribution (Point params.next)) (evaluatedPointFamilyLeft params family)
(evaluatedPointFamilyRight params family) zeta)
:
SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.1)
(fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyRight params family q.1) zeta
Pull a single-point evaluated-family self-consistency bound up to the first coordinate of an evaluated-slice question.
theorem
MIPStarRE.LDT.Commutativity.evaluatedPointSelfConsistency_snd
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(zeta : Error)
(hssc :
SDDRel strategy.state (uniformDistribution (Point params.next)) (evaluatedPointFamilyLeft params family)
(evaluatedPointFamilyRight params family) zeta)
:
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
Pull a single-point evaluated-family self-consistency bound up to the second coordinate of an evaluated-slice question.