Documentation

MIPRE.Background.LIDT.Co.Pasting.ComparisonLemmas.CommuteGHalfSandwich.MoveChain.FlatChain

Section 12 pasting: half-sandwich flat chain #

The post-move and combined flat chains used after the distinguished completed-slice factor has been moved to the right tensor register, alternating between pairwise commutation and self-consistency steps: the counterpart of the vendored file of the same path under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The chain lengths, the error sequences and their sums are classical and imported from the vendored file. The two families take the symmetric model S : SymModel 𝔓 K as their first explicit argument, as the placed families of Setup/Definitions and MoveChain/Lifting do: commuteGHalfSandwich_postMoveFlatFamily S params family r i and commuteGHalfSandwich_flatChainFamily S params family r i. The outcome identities, whose vendored versions have no state, take S second, after params, as commuteGHalfSandwich_moveChainFamily_zero does. No vendored lemma here has a swap, density or normalization hypothesis.

The recursions unfold by ite_eq_left, ite_eq_right, dite_eq_left and dite_eq_right (the current names of the deprecated if_pos, if_neg, dif_pos, dif_neg), and the outcome identities hold by S.leftTensor_one, S.rightTensor_one, S.leftTensor_mul_leftTensor and association up to definitional equality, where the vendored proofs unfold by simp; the last family of the post-move chain is reached by induction through commuteGHalfSandwich_prefixSecondSliceLeft_splitSuccLift_eq_secondSliceLift, as in the vendored proof, with the index Fin.last reached by definitional equality.

Not ported #

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

Post-move flat chain and flat-chain families #

source
noncomputable def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_postMoveFlatFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) :
Fin (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatLength r + 1) → IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)

Operator-family sequence for the post-move part of the flat chain.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_flatChainFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) :
    Fin (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainLength r + 1) → IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)

    Operator-family sequence obtained by concatenating the move chain and the post-move flat chain.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_commuteFamily_zero_eq_recursiveTarget {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params 0) (ogs : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params 0) :
      (commuteGHalfSandwich_commuteFamily S params family 0 q).outcome ogs = (commuteGHalfSandwich_recursiveTargetFamily S params family 0 q).outcome ogs

      With no tail, the commuted endpoint is the recursive target.

      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_secondSliceLift_recursiveTarget {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (ogs : MIPStarRE.LDT.Pasting.MoveO params (r + 1)) :
      (commuteGHalfSandwich_secondSliceLiftFamily S params family r (commuteGHalfSandwich_recursiveTargetFamily S params family r) q).outcome ogs = (commuteGHalfSandwich_recursiveTargetFamily S params family (r + 1) q).outcome ogs

      The second-slice lift of the r-step recursive target is the (r + 1)-step recursive target.

      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_postMoveFlatFamily_zero_active {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params r) (ogs : MIPStarRE.LDT.Pasting.MoveO params r) :
      (commuteGHalfSandwich_postMoveFlatFamily S params family r 0 q).outcome ogs = (commuteGHalfSandwich_moveFamily S params family r q).outcome ogs

      The first family of the post-move flat chain is the move family.

      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_postMoveFlatFamily_one_active {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (ogs : MIPStarRE.LDT.Pasting.MoveO params (r + 1)) :
      (commuteGHalfSandwich_postMoveFlatFamily S params family (r + 1) ⟨1, ⋯⟩ q).outcome ogs = (commuteGHalfSandwich_commuteFamily S params family (r + 1) q).outcome ogs

      The second family of the post-move flat chain of length r + 1 is the commuted endpoint.

      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_postMoveFlatFamily_last_active {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params r) (ogs : MIPStarRE.LDT.Pasting.MoveO params r) :
      (commuteGHalfSandwich_postMoveFlatFamily S params family r (Fin.last (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatLength r)) q).outcome ogs = (commuteGHalfSandwich_recursiveTargetFamily S params family r q).outcome ogs

      The last family of the post-move flat chain is the recursive target.

      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_flatChainFamily_zero {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params r) (ogs : MIPStarRE.LDT.Pasting.MoveO params r) :
      (commuteGHalfSandwich_flatChainFamily S params family r 0 q).outcome ogs = (commuteGHalfSandwich_moveSourceFamily S params family r q).outcome ogs

      The first family of the flat chain is the move source.

      source
      theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_flatChainFamily_last {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params r) (ogs : MIPStarRE.LDT.Pasting.MoveO params r) :
      (commuteGHalfSandwich_flatChainFamily S params family r (Fin.last (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainLength r)) q).outcome ogs = (commuteGHalfSandwich_recursiveTargetFamily S params family r q).outcome ogs

      The last family of the flat chain is the recursive target.