Documentation

MIPStarRE.LDT.Pasting.Bernoulli.FromHToG.PaperMoveChain.Telescope

Section 12 pasting: from-H-to-G paper telescope #

This file assembles the adjacent-stage paper move chain and records the final stage-mass telescope for the fromHToG reduction.

source
theorem MIPStarRE.LDT.Pasting.fromHToGAdjacentStage_paperMoveChain {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hfacts : GHatFactsStatement params ψbi family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params ψbi family) (k ℓ : ℕ) (hℓ : ℓ < k) :
|fromHToGStageMass params ψbi family k ℓ - fromHToGStageMass params ψbi family k (ℓ + 1)| ≤ fromHToGRecurrenceError params gamma zeta k

One adjacent fromHToG paper step.

source
theorem MIPStarRE.LDT.Pasting.fromHToG_recurrenceStep_of_paperMoveChain {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hfacts : GHatFactsStatement params ψbi family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params ψbi family) (k ℓ : ℕ) :
ℓ < k → |fromHToGStageMass params ψbi family k ℓ - fromHToGStageMass params ψbi family k (ℓ + 1)| ≤ fromHToGRecurrenceError params gamma zeta k

Adjacent-stage recurrence obtained by applying the paper move chain at every nonterminal stage.

source
theorem MIPStarRE.LDT.Pasting.fromHToG_stageMassTelescope_of_paperMoveChain {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hfacts : GHatFactsStatement params ψbi family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params ψbi family) (k : ℕ) :
|fromHToGStageMass params ψbi family k 0 - fromHToGStageMass params ψbi family k k| ≤ fromHToGPaperTotalError params gamma zeta k

The paper-total stage-mass telescope for fromHToG.

This follows the iteration in ld-pasting.tex:1354--1372: applying the adjacent-stage estimate over all k stages gives k copies of the per-stage error. Lean records that literal telescope before the final scalar bound fromHToGPaperTotalError_le absorbs it into fromHToGError.