Section 12 pasting: commute G half-sandwich move lemmas #
This module contains the move-chain lemmas for the half-sandwich commutation
chain. The split reindexing lemmas and the two-term base case are kept in
StepLemmas.Split.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
theorem
MIPStarRE.LDT.Pasting.gHatSelfConsistency_sddOpRel_quadThird
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(zeta : Error)
(r : ℕ)
(hsc :
SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family)
(gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta))
:
SDDOpRel ψbi
(uniformDistribution (SliceQuestion params × SliceQuestion params × SliceQuestion params × PointTuple params r))
(fun (q : SliceQuestion params × SliceQuestion params × SliceQuestion params × PointTuple params r) =>
(gHatSelfConsistencyLeftFamily params family).toIdxOpFamily q.2.2.1)
(fun (q : SliceQuestion params × SliceQuestion params × SliceQuestion params × PointTuple params r) =>
(gHatSelfConsistencyRightFamily params family).toIdxOpFamily q.2.2.1)
(gHatSelfConsistencyError zeta)
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_step_commute
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(r : ℕ)
(hcom :
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (gHatPairProductLeft params family)
(gHatPairProductRight params family) (gHatCommutationError params gamma zeta))
:
SDDOpRel ψbi (uniformDistribution (SliceQuestion params × SliceQuestion params × PointTuple params r))
(commuteGHalfSandwich_moveFamily params family r) (commuteGHalfSandwich_commuteFamily params family r)
(gHatCommutationError params gamma zeta)
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_prefixFirstSliceLeft_move
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(r : ℕ)
(δ : Error)
(hAB :
SDDOpRel ψbi (uniformDistribution (SliceQuestion params × SliceQuestion params × PointTuple params r))
(commuteGHalfSandwich_moveSourceFamily params family r) (commuteGHalfSandwich_moveFamily params family r) δ)
:
SDDOpRel ψbi
(uniformDistribution (SliceQuestion params × SliceQuestion params × SliceQuestion params × PointTuple params r))
(commuteGHalfSandwich_moveStepSourceFamily params family r) (commuteGHalfSandwich_moveStepMidFamily params family r) δ
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveStepMid_toTarget
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(zeta : Error)
(r : ℕ)
(hsc :
SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family)
(gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta))
:
SDDOpRel ψbi
(uniformDistribution (SliceQuestion params × SliceQuestion params × SliceQuestion params × PointTuple params r))
(commuteGHalfSandwich_moveStepMidFamily params family r) (commuteGHalfSandwich_moveStepTargetFamily params family r)
(gHatSelfConsistencyError zeta)