Section 12 pasting: commute G half-sandwich split lemmas #
This module contains the split reindexing lemmas and the two-term base case for the half-sandwich commutation chain.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_split_iff
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(k : ℕ)
(δ : Error)
:
SDDOpRel ψbi (uniformDistribution (PointTuple params (k + 1))) (gHatHalfSandwichLeft params family (k + 1))
(gHatHalfSandwichRight params family (k + 1)) δ ↔ SDDOpRel ψbi (uniformDistribution (SliceQuestion params × PointTuple params k))
(headTailOrderedFamily params family k) (headTailRotatedFamily params family k) δ
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_split_one_iff
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(δ : Error)
:
SDDOpRel ψbi (uniformDistribution (SliceQuestion params × PointTuple params 1)) (headTailOrderedFamily params family 1)
(headTailRotatedFamily params family 1) δ ↔ SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (gHatPairProductLeft params family)
(gHatPairProductRight params family) δ
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_core_two
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(hcom :
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (gHatPairProductLeft params family)
(gHatPairProductRight params family) (gHatCommutationError params gamma zeta))
:
SDDOpRel ψbi (uniformDistribution (PointTuple params 2)) (gHatHalfSandwichLeft params family 2)
(gHatHalfSandwichRight params family 2) (commuteGHalfSandwichError params gamma zeta 2)