Section 12 pasting: commute G half-sandwich setup — sum bounds #
Sum-of-adjoint-products ≤ 1 bounds for the half-product, reverse-half-product,
pair-prefix, and bipartite tensor families. Also contains the error-envelope bound
commuteGHalfSandwich_error_bound and its helper rpow_oneSixteenth_nonneg.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
Half-product sum bounds #
theorem
MIPStarRE.LDT.Pasting.gHatHalfProduct_sum_adjoint_mul_le_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(xs : PointTuple params r)
:
∑ gs : GHatTupleOutcome params r,
Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family r xs gs) * gHatHalfProductOutcomeOperator params family r xs gs ≤ 1
theorem
MIPStarRE.LDT.Pasting.gHatReverseHalfProduct_sum_adjoint_mul_le_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(xs : PointTuple params r)
:
∑ gs : GHatTupleOutcome params r,
Matrix.conjTranspose (gHatReverseHalfProductOutcomeOperator params family r xs gs) * gHatReverseHalfProductOutcomeOperator params family r xs gs ≤ 1
Error-envelope bound #
The fixed paper exponent 1/16 keeps Real.rpow nonnegative even on the
negative branch, because cos (π / 16) > 0. This lets the commuteGHalfSandwich
error envelopes avoid threading an extra 0 ≤ gamma hypothesis.
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_error_bound
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(k : ℕ)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le : zeta ≤ 1)
:
3 * ↑k * (4 * ↑k * zeta + ↑k * gHatCommutationError params gamma zeta) ≤ commuteGHalfSandwichError params gamma zeta k
Pair-prefix and bipartite tensor bounds #
theorem
MIPStarRE.LDT.Pasting.gHatPairPrefix_sum_adjoint_mul_le_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(q : SlicePairQuestion params)
:
∑ og : GHatOutcome params × GHatOutcome params,
((gHatIdxMeas params family q.1).outcome og.1 * (gHatIdxMeas params family q.2).outcome og.2).conjTranspose * ((gHatIdxMeas params family q.1).outcome og.1 * (gHatIdxMeas params family q.2).outcome og.2) ≤ 1
theorem
MIPStarRE.LDT.Pasting.leftTensor_rightTensor_sum_adjoint_mul_le_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{α : Type u_2}
{β : Type u_3}
[Fintype α]
[Fintype β]
(prefixOp : α → Quantum.Op ι)
(tailOp : β → Quantum.Op ι)
(hprefix : ∑ a : α, Matrix.conjTranspose (prefixOp a) * prefixOp a ≤ 1)
(htail : ∑ b : β, Matrix.conjTranspose (tailOp b) * tailOp b ≤ 1)
:
∑ ag : α × β,
(leftTensor (prefixOp ag.1) * rightTensor (tailOp ag.2)).conjTranspose * (leftTensor (prefixOp ag.1) * rightTensor (tailOp ag.2)) ≤ 1
Generic tensor-contraction bound: if prefixOp : α → Op ι and
tailOp : β → Op ι each satisfy ∑ (·)ᴴ * (·) ≤ 1, then the joint family
leftTensor (prefixOp a) * rightTensor (tailOp b) on α × β also satisfies
∑ (·)ᴴ * (·) ≤ 1 on the bipartite space.