Helper strong self-consistency bounds: post-delete transports #
Post-delete-an-A transport lemmas culminating in the moved-quantity bound
used before the residual-chain assembly.
References #
references/ldt-paper/self_improvement.texblueprint/src/chapter/ch07_self_improvement.tex
Post-delete-an-A transports #
theorem
MIPStarRE.LDT.SelfImprovement.helperDeleteAQuantity_abs_sub_clonedQuantity_le_sqrt
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params ι)
(eps delta : Error)
(T : SubMeas (Polynomial params) ι)
(hlocal :
∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError params eps delta)
:
|helperDeleteAQuantity params strategy T - helperDeleteAClonedQuantity params strategy T| ≤ √(selfImprovementVarianceError params eps delta)
Paper eq:swap-u-for-v-attack-of-the-clones: after delete-an-A, the
remaining point projector may be evaluated at an independent point at cost
√ζ_variance.
theorem
MIPStarRE.LDT.SelfImprovement.helperDeleteAClonedQuantity_abs_sub_moveOverVQuantity_le_sqrt_two_delta
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params ι)
(delta : Error)
(T : SubMeas (Polynomial params) ι)
(hssc :
BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta)
:
|helperDeleteAClonedQuantity params strategy T - helperMoveOverVQuantity params strategy T| ≤ √(2 * delta)
Paper eq:move-over-v: the cloned delete-an-A quantity can be moved to
the right tensor factor at cost √(2δ) from point self-consistency.