Section 12 pasting: from-H-to-G theorem #
Derivation of lem:from-H-to-G, from the G-hat facts, the half-sandwich
commutation theorem, and the telescoping Bernoulli-stage comparison.
theorem
MIPStarRE.LDT.Pasting.fromHToG_ofGHatFactsAndHalfSandwich
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(ψbi : QuantumState (ι × ι))
(hnorm : ψbi.IsNormalized)
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le_one : zeta ≤ 1)
(hfacts : GHatFactsStatement params ψbi family gamma zeta)
(hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j)
(k : ℕ)
:
FromHToGStatement params strategy ψbi family gamma zeta k
Internal form of lem:from-H-to-G after applying cor:G-hat-facts and
lem:commute-g-half-sandwich.
Source: The proof in references/ldt-paper/ld-pasting.tex:1295-1670
uses the completed-measurement facts and the half-sandwich commutation theorem
internally. The paper-facing theorem fromHToG below derives those inputs
from the source hypotheses.
theorem
MIPStarRE.LDT.Pasting.fromHToG_ofGHatFacts
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(ψbi : QuantumState (ι × ι))
(hnorm : ψbi.IsNormalized)
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le_one : zeta ≤ 1)
(hfacts : GHatFactsStatement params ψbi family gamma zeta)
(k : ℕ)
:
FromHToGStatement params strategy ψbi family gamma zeta k
Internal form of lem:from-H-to-G from cor:G-hat-facts.
The half-sandwich estimates are obtained from the same G-hat facts.
theorem
MIPStarRE.LDT.Pasting.fromHToG_ofComMain
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(hgamma_nonneg : 0 ≤ gamma)
(hgamma_le : gamma ≤ 1)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le_one : zeta ≤ 1)
(hdq_le : params.d ≤ params.q)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hcom : Commutativity.ComMainConclusion params strategy family gamma zeta)
(k : ℕ)
:
FromHToGStatement params strategy strategy.state family gamma zeta k
Internal form of lem:from-H-to-G from the Section 11 commutativity
conclusion.
theorem
MIPStarRE.LDT.Pasting.fromHToG
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(eps delta gamma zeta : Error)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hgamma_le : gamma ≤ 1)
(hzeta_le_one : zeta ≤ 1)
(hdq_le : params.d ≤ params.q)
(hgood : strategy.IsGood eps delta gamma)
(hcons : family.ConsistentWithPoints strategy zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta)
(k : ℕ)
:
FromHToGStatement params strategy strategy.state family gamma zeta k
lem:from-H-to-G, source-facing form at the strategy state.