Documentation

MIPRE.Background.LIDT.Co.Pasting.SwitcherooSetup.Terms

Section 12 pasting: switcheroo aggregate terms #

The remaining switcheroo aggregate terms and split formulas: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooSetup/Terms.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored second bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; the slice family is an IdxPolyFamily params 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓.

switcherooAggregateThirdTerm_eq_fourthTerm takes the adjoint in the local algebra, through S.ev_conjTranspose and S.leftTensor_conjTranspose, in place of the vendored conjTranspose_opTensor with the identity, and the Hermitian facts come from IsSelfAdjoint.of_nonneg rather than Matrix.PosSemidef. switcherooAggregateFourthTerm_eq_split inserts G = ∑_g G_g G_g in the local algebra and pulls the sum out through S.leftTensor_finset_sum and S.ev_sum.

Not ported #

Nothing: every declaration of the vendored file is ported here.

References #

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

source
noncomputable def MIPRE.LIDT.Co.Pasting.completePartProjFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) :
IdxProjSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Unit 𝔓

The one-outcome projective family whose sole effect is the complete slice part G^x.

Equations
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateSecondTerm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) :
    ℝ

    The second positive term in the switcheroo expansion.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateThirdTerm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) :
      ℝ

      The third (negative) term in the switcheroo expansion.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) :
        ℝ

        The fourth (negative) term in the switcheroo expansion.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateThirdTerm_eq_fourthTerm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) :
          switcherooAggregateThirdTerm params S family M = switcherooAggregateFourthTerm params S family M

          The third and fourth switcheroo terms agree: their summands are adjoint to each other.

          source
          theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_eq_split {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) :
          switcherooAggregateFourthTerm params S family M = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => ∑ go : MIPStarRE.LDT.Polynomial params × Outcome, S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))

          Split the fourth switcheroo term by inserting the complete-part projector resolution G = ∑_g G_g.