Documentation

MIPRE.Background.LIDT.Co.Test.MainTheorem.TwoSpace

The two-space calculus of the main theorem's tail #

The tail of the vendored main theorem (Test/MainTheorem/SourceRoleRegister/* and Test/MainTheorem/MainFormal.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/) runs on the strategy's own state, a state on ιA × ιB with Alice's measurements on ιA and Bob's on ιB. In the port of planning/c6b-plan.md (milestone M13) that state is the strategy's bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ, whose players' algebras 𝒜 and ℬ are abstract star-ordered ⋆-algebras, as in Co ProjStrat and in MIPRE.LIDT.Simul.SoundIn, not C⋆-algebras. This file holds the two-space calculus the tail needs there. It has no vendored counterpart.

Why it is needed. The doubled model D(M) (Co/Doubling/) gives only role averages: Doubling.bipartiteConsError_model says bc_D(X, Y) = ½ (bc_M(X¹, Y²) + bc_M(Y¹, X²)), so pulling a one-sided relation back from D(M) costs a factor two, which breaks the vendored scalar cascade into mainFormalError. Milestone M3 narrowed the vendored _heterogeneous lemmas of Preliminaries to one carrier (planning/c6b-plan.md, "Departures in M3 and M5"); their two-space forms are here, under their vendored names in the namespace MIPRE.LIDT.Co.TwoSpace.

Vocabulary.

Completion in an abstract algebra. Co Preliminaries.completeAtOutcome is generic, but completeAtOutcomeProj and ProjMeas.isPVMIn need a C⋆-algebra. In a finite pair the players' algebras are ⋆-isomorphic to the commutants of the other player's operators (IsFinitePair.equivA, equivB, MIPRE/Foundations/FinitePairOrder.lean), which are C⋆-algebras; completeAtOutcomeProjA and completeAtOutcomeProjB complete there and come back along the inverse. Positivity transfers along any ⋆-homomorphism of star-ordered rings, and projectivity and the total are algebraic, so the order agreement of a finite pair is not used. ProjMeas.isPVMIn_of_isFinitePair (in the namespace MIPRE.LIDT.Co.ProjMeas, for dot notation) is the same transport for ProjMeas.isPVMIn.

New here #

Every declaration of this file is new; it has no vendored counterpart.

Not ported #

Nothing: the file has no vendored counterpart.

Placements #

source
noncomputable def MIPRE.LIDT.Co.TwoSpace.placeA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) :
𝒜 →⋆ₐ[ℂ] M.H →L[ℂ] M.H

The first player's placement a ↦ π (πA a) into the operators of M.H.

Equations
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.TwoSpace.placeB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) :
    ℬ →⋆ₐ[ℂ] M.H →L[ℂ] M.H

    The second player's placement b ↦ π (πB b) into the operators of M.H.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LIDT.Co.TwoSpace.placeA_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) :
      (placeA M) a = M.π (M.πA a)

      placeA M a is π (πA a).

      source
      @[simp]
      theorem MIPRE.LIDT.Co.TwoSpace.placeB_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (b : ℬ) :
      (placeB M) b = M.π (M.πB b)

      placeB M b is π (πB b).

      source
      def MIPRE.LIDT.Co.TwoSpace.vecState {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hψ : ‖M.ψ‖ = 1) :
      VecState M.H

      The vector state of a unit state of M.

      Equations
      Instances For
        source
        @[simp]
        theorem MIPRE.LIDT.Co.TwoSpace.vecState_Ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hψ : ‖M.ψ‖ = 1) :
        (vecState M hψ).Ψ = M.ψ

        The vector of vecState M hψ is M.ψ.

        source
        theorem MIPRE.LIDT.Co.TwoSpace.bornProb_eq_ev {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hψ : ‖M.ψ‖ = 1) (a : 𝒜) (b : ℬ) :
        M.bornProb a b = (vecState M hψ).ev ((placeA M) a * (placeB M) b)

        The Born probability is the expectation of the product of the placements.

        source
        noncomputable def MIPRE.LIDT.Co.TwoSpace.leftPlacedSubMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {α : Type u_4} [Fintype α] (A : SubMeas α 𝒜) :
        SubMeas α (M.H →L[ℂ] M.H)

        A submeasurement of the first player's algebra, placed on M.H (the vendored leftPlacedSubMeas (ιB := ιB)).

        Equations
        Instances For
          source
          @[simp]
          theorem MIPRE.LIDT.Co.TwoSpace.leftPlacedSubMeas_outcome {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {α : Type u_4} [Fintype α] (A : SubMeas α 𝒜) (a : α) :
          (leftPlacedSubMeas M A).outcome a = M.π (M.πA (A.outcome a))

          The outcome operators of a left-placed submeasurement are placed.

          source
          @[simp]
          theorem MIPRE.LIDT.Co.TwoSpace.leftPlacedSubMeas_total {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {α : Type u_4} [Fintype α] (A : SubMeas α 𝒜) :
          (leftPlacedSubMeas M A).total = M.π (M.πA A.total)

          The total of a left-placed submeasurement is placed.

          source
          noncomputable def MIPRE.LIDT.Co.TwoSpace.placeLeft {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (A : IdxSubMeas Question Outcome 𝒜) :
          IdxSubMeas Question Outcome (M.H →L[ℂ] M.H)

          A family of submeasurements of the first player's algebra, placed on M.H (the vendored IdxSubMeas.placeLeft (ιB := ιB)).

          Equations
          Instances For
            source
            theorem MIPRE.LIDT.Co.TwoSpace.qSDD_leftPlaced_eq_sum_norm_sq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (A P : SubMeas Outcome 𝒜) :
            (vecState M hψ).qSDD (leftPlacedSubMeas M A) (leftPlacedSubMeas M P) = ∑ a : Outcome, ‖(M.π (M.πA (A.outcome a - P.outcome a))) M.ψ‖ ^ 2

            The squared distance of two placed submeasurements of the first player is the sum of norms ∑ₐ ‖π(πA(Aₐ − Pₐ)) ψ‖² with which M8's heterogeneous orthonormalization concludes.

            source
            noncomputable def MIPRE.LIDT.Co.TwoSpace.rightPlacedSubMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] [StarOrderedRing ℬ] {α : Type u_4} [Fintype α] (B : SubMeas α ℬ) :
            SubMeas α (M.H →L[ℂ] M.H)

            A submeasurement of the second player's algebra, placed on M.H (the vendored rightPlacedSubMeas (ιA := ιA)).

            Equations
            Instances For
              source
              @[simp]
              theorem MIPRE.LIDT.Co.TwoSpace.rightPlacedSubMeas_outcome {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] [StarOrderedRing ℬ] {α : Type u_4} [Fintype α] (B : SubMeas α ℬ) (a : α) :
              (rightPlacedSubMeas M B).outcome a = M.π (M.πB (B.outcome a))

              The outcome operators of a right-placed submeasurement are placed.

              source
              @[simp]
              theorem MIPRE.LIDT.Co.TwoSpace.rightPlacedSubMeas_total {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] [StarOrderedRing ℬ] {α : Type u_4} [Fintype α] (B : SubMeas α ℬ) :
              (rightPlacedSubMeas M B).total = M.π (M.πB B.total)

              The total of a right-placed submeasurement is placed.

              source
              noncomputable def MIPRE.LIDT.Co.TwoSpace.placeRight {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] [StarOrderedRing ℬ] {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (B : IdxSubMeas Question Outcome ℬ) :
              IdxSubMeas Question Outcome (M.H →L[ℂ] M.H)

              A family of submeasurements of the second player's algebra, placed on M.H (the vendored IdxSubMeas.placeRight (ιA := ιA)).

              Equations
              Instances For
                source
                theorem MIPRE.LIDT.Co.TwoSpace.qSDD_rightPlaced_eq_sum_norm_sq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (B P : SubMeas Outcome ℬ) :
                (vecState M hψ).qSDD (rightPlacedSubMeas M B) (rightPlacedSubMeas M P) = ∑ a : Outcome, ‖(M.π (M.πB (B.outcome a - P.outcome a))) M.ψ‖ ^ 2

                The squared distance of two placed submeasurements of the second player is ∑ₐ ‖π(πB(Bₐ − Pₐ)) ψ‖².

                Bridges to the two-space defect #

                source
                theorem MIPRE.LIDT.Co.TwoSpace.qBipartiteMatchMass_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (A : SubMeas Outcome 𝒜) (B : SubMeas Outcome ℬ) :
                qBipartiteMatchMass M A B = (vecState M hψ).qMatchMass (leftPlacedSubMeas M A) (rightPlacedSubMeas M B)

                M2's two-space matching mass is the matching mass of the placed submeasurements.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.qBipartiteConsDefect_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (A : SubMeas Outcome 𝒜) (B : SubMeas Outcome ℬ) :
                qBipartiteConsDefect M A B = (vecState M hψ).qConsDefect (leftPlacedSubMeas M A) (rightPlacedSubMeas M B)

                M2's two-space consistency defect is the consistency defect of the placed submeasurements.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.bipartiteConsError_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝒜) (B : IdxSubMeas Question Outcome ℬ) :
                bipartiteConsError M 𝒟 A B = (vecState M hψ).consError 𝒟 (placeLeft M A) (placeRight M B)

                M2's averaged two-space defect is the averaged consistency defect of the placed families.

                Positivity #

                source
                theorem MIPRE.LIDT.Co.TwoSpace.bornProb_le_qform_πA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {x : 𝒜} {y : ℬ} (hx : 0 ≤ x) (hy : y ≤ 1) :
                M.bornProb x y ≤ M.qform (M.πA x)

                ⟨ψ, (x ⊗ y) ψ⟩ ≤ ⟨ψ, (x ⊗ 1) ψ⟩ for 0 ≤ x and y ≤ 1: x ⊗ (1 − y) is a product of commuting positive operators.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.bornProb_le_qform_πB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {x : 𝒜} {y : ℬ} (hx : x ≤ 1) (hy : 0 ≤ y) :
                M.bornProb x y ≤ M.qform (M.πB y)

                ⟨ψ, (x ⊗ y) ψ⟩ ≤ ⟨ψ, (1 ⊗ y) ψ⟩ for x ≤ 1 and 0 ≤ y (bornProb_le_qform_πA for the swapped model).

                source
                theorem MIPRE.LIDT.Co.TwoSpace.qBipartiteConsDefect_le_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (A : SubMeas Outcome 𝒜) (B : SubMeas Outcome ℬ) :
                qBipartiteConsDefect M A B ≤ 1

                A two-space consistency defect is at most 1 at a unit state.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.bipartiteConsError_le_one_of_isProbability {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : 𝒟.IsProbability) (A : IdxSubMeas Question Outcome 𝒜) (B : IdxSubMeas Question Outcome ℬ) :
                bipartiteConsError M 𝒟 A B ≤ 1

                Under a probability question distribution, the averaged two-space defect is at most 1.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.bipartiteConsError_uniform_le_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (A : IdxSubMeas Question Outcome 𝒜) (B : IdxSubMeas Question Outcome ℬ) :
                bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Question) A B ≤ 1

                Under the uniform question distribution, the averaged two-space defect is at most 1 (the trivial branch of the main theorem).

                Consistency and distance #

                source
                theorem MIPRE.LIDT.Co.TwoSpace.questionSDD_placeLeft_placeRight_le_two_questionConsistency {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (A : Measurement Outcome 𝒜) (B : Measurement Outcome ℬ) :
                (vecState M hψ).qSDD (leftPlacedSubMeas M A.toSubMeas) (rightPlacedSubMeas M B.toSubMeas) ≤ 2 * qBipartiteConsDefect M A.toSubMeas B.toSubMeas

                For measurements A of 𝒜 and B of ℬ, the squared distance of their placements is at most twice their two-space consistency defect: the per-question core of simeqToApprox_heterogeneous, which is BipartiteModel.xSqNorm_sum_le_two_mul.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.simeqToApprox_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxMeas Question Outcome 𝒜) (B : IdxMeas Question Outcome ℬ) (δ : ℝ) :
                bipartiteConsError M 𝒟 A.toIdxSubMeas B.toIdxSubMeas ≤ δ → (vecState M hψ).SDDRel 𝒟 (placeLeft M A.toIdxSubMeas) (placeRight M B.toIdxSubMeas) (2 * δ)

                Heterogeneous prop:simeq-to-approx: two-space consistency of measurements A of 𝒜 and B of ℬ at δ gives the state-dependent distance 2δ between their placements.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.two_questionConsistency_eq_questionSDD_of_projective {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] (A : ProjMeas Outcome 𝒜) (B : ProjMeas Outcome ℬ) :
                2 * qBipartiteConsDefect M A.toSubMeas B.toSubMeas = (vecState M hψ).qSDD (leftPlacedSubMeas M A.toSubMeas) (rightPlacedSubMeas M B.toSubMeas)

                For projective measurements A of 𝒜 and B of ℬ, twice their two-space consistency defect is the squared distance of their placements: the two placements commute and each is idempotent, so (Aₐ ⊗ 1 − 1 ⊗ Bₐ)² = Aₐ ⊗ 1 + 1 ⊗ Bₐ − 2 Aₐ ⊗ Bₐ. Algebraic: no C⋆-structure on 𝒜 or ℬ is used.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.approxToSimeq_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxProjMeas Question Outcome 𝒜) (B : IdxProjMeas Question Outcome ℬ) (δ : ℝ) :
                (vecState M hψ).SDDRel 𝒟 (placeLeft M A.toIdxSubMeas) (placeRight M B.toIdxSubMeas) (2 * δ) → bipartiteConsError M 𝒟 A.toIdxSubMeas B.toIdxSubMeas ≤ δ

                Heterogeneous projective converse of prop:simeq-to-approx: for projective measurements A of 𝒜 and B of ℬ, the state-dependent distance 2δ between their placements gives two-space consistency at δ.

                Triangle inequalities #

                source
                theorem MIPRE.LIDT.Co.TwoSpace.consRel_of_matchGap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A A' : IdxSubMeas Question Outcome 𝒜) (B B' : IdxSubMeas Question Outcome ℬ) (s e : Question → ℝ) (δ ε η : ℝ) (hAB : bipartiteConsError M 𝒟 A B ≤ δ) (hgap : ∀ (q : Question), |qBipartiteMatchMass M (A q) (B q) - qBipartiteMatchMass M (A' q) (B' q)| ≤ √(s q)) (hs : ∀ (q : Question), 0 ≤ s q) (hsε : MIPStarRE.LDT.avgOver 𝒟 s ≤ ε) (he : ∀ (q : Question), max 0 (M.bornProb (A' q).total (B' q).total - M.bornProb (A q).total (B q).total) ≤ e q) (heη : MIPStarRE.LDT.avgOver 𝒟 e ≤ η) :
                bipartiteConsError M 𝒟 A' B' ≤ δ + √ε + η

                The common substitution step of the two-space triangleSub family (Co Preliminaries.consRel_of_matchGap): if bipartiteConsError M 𝒟 A B ≤ δ, the matching masses of (A, B) and (A', B') differ by at most √(s q) at each question, and the total overlap of (A', B') exceeds that of (A, B) by at most e q, then the defect of (A', B') is at most δ + √ε + η for 𝔼 s ≤ ε and 𝔼 e ≤ η.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.triangleSub_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxMeas Question Outcome 𝒜) (C : IdxSubMeas Question Outcome ℬ) (δ ε : ℝ) (hAC : bipartiteConsError M 𝒟 A.toIdxSubMeas C ≤ δ) (hAB : (vecState M hψ).SDDRel 𝒟 (placeLeft M A.toIdxSubMeas) (placeLeft M B.toIdxSubMeas) ε) :
                bipartiteConsError M 𝒟 B.toIdxSubMeas C ≤ δ + √ε

                Heterogeneous left substitution (prop:triangle-sub): if measurements A of 𝒜 and a submeasurement C of ℬ are consistent at δ, and the placements of A and of a measurement B of 𝒜 are at state-dependent distance ε, then B and C are consistent at δ + √ε.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.triangleSub_right_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question Outcome 𝒜) (B D : IdxMeas Question Outcome ℬ) (δ ε : ℝ) (hAB : bipartiteConsError M 𝒟 A B.toIdxSubMeas ≤ δ) (hBD : (vecState M hψ).SDDRel 𝒟 (placeRight M B.toIdxSubMeas) (placeRight M D.toIdxSubMeas) ε) :
                bipartiteConsError M 𝒟 A D.toIdxSubMeas ≤ δ + √ε

                Heterogeneous right substitution: if a submeasurement A of 𝒜 and a measurement B of ℬ are consistent at δ, and the placements of B and of a measurement D of ℬ are at state-dependent distance ε, then A and D are consistent at δ + √ε.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.simeqTriangleInequality_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A C : IdxMeas Question Outcome 𝒜) (B D : IdxMeas Question Outcome ℬ) (ε δ γ : ℝ) (hAB : bipartiteConsError M 𝒟 A.toIdxSubMeas B.toIdxSubMeas ≤ ε) (hCB : bipartiteConsError M 𝒟 C.toIdxSubMeas B.toIdxSubMeas ≤ δ) (hCD : bipartiteConsError M 𝒟 C.toIdxSubMeas D.toIdxSubMeas ≤ γ) :
                bipartiteConsError M 𝒟 A.toIdxSubMeas D.toIdxSubMeas ≤ ε + 2 * √(δ + γ)

                Heterogeneous prop:simeq-triangle-inequality, with the vendored constant: for measurements A, C of 𝒜 and B, D of ℬ, consistency of (A, B) at ε, of (C, B) at δ and of (C, D) at γ gives consistency of (A, D) at ε + 2√(δ + γ). As in Co Preliminaries.simeqTriangleInequality: compare the placements of B and D through C, then substitute on the right.

                Data processing #

                source
                theorem MIPRE.LIDT.Co.TwoSpace.qBipartiteMatchMass_postprocess_ge {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (A : SubMeas α 𝒜) (B : SubMeas α ℬ) (f : α → β) :
                qBipartiteMatchMass M A B ≤ qBipartiteMatchMass M (postprocess A f) (postprocess B f)

                Postprocessing two submeasurements, of 𝒜 and of ℬ, by the same readout map can only increase their two-space matching mass: the new terms are the old ones plus Born probabilities of positive elements within each fibre.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.qBipartiteConsDefect_postprocess_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (A : SubMeas α 𝒜) (B : SubMeas α ℬ) (f : α → β) :
                qBipartiteConsDefect M (postprocess A f) (postprocess B f) ≤ qBipartiteConsDefect M A B

                Postprocessing two submeasurements, of 𝒜 and of ℬ, by the same readout map can only decrease their two-space consistency defect: the totals are kept.

                source
                theorem MIPRE.LIDT.Co.TwoSpace.consRelDataProcessing_questionDependent {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Question : Type u_4} {α : Type u_5} {β : Type u_6} [Fintype α] [Fintype β] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question α 𝒜) (B : IdxSubMeas Question α ℬ) (δ : ℝ) (f : Question → α → β) :
                bipartiteConsError M 𝒟 A B ≤ δ → (bipartiteConsError M 𝒟 (fun (q : Question) => postprocess (A q) (f q)) fun (q : Question) => postprocess (B q) (f q)) ≤ δ

                Question-dependent postprocessing preserves two-space consistency (the two-space form of Co Preliminaries.consRelDataProcessing_questionDependent).

                Completion in the players' algebras of a finite pair #

                source
                noncomputable def MIPRE.LIDT.Co.TwoSpace.completeAtOutcomeProjA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (P : ProjSubMeas Outcome 𝒜) (a0 : Outcome) :
                ProjMeas Outcome 𝒜

                Complete a projective submeasurement of the first player's algebra of a finite pair at a distinguished outcome, to a projective measurement: Co Preliminaries.completeAtOutcomeProj in the commutant IsFinitePair.equivA identifies 𝒜 with, a C⋆-algebra, carried back along the inverse.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem MIPRE.LIDT.Co.TwoSpace.completeAtOutcomeProjA_toMeasurement {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (P : ProjSubMeas Outcome 𝒜) (a0 : Outcome) :
                  (completeAtOutcomeProjA hM P a0).toMeasurement = Preliminaries.completeAtOutcome P.toSubMeas a0

                  The measurement of completeAtOutcomeProjA hM P a0 is the canonical completion completeAtOutcome P.toSubMeas a0 in 𝒜.

                  source
                  theorem MIPRE.LIDT.Co.TwoSpace.completeAtOutcomeProjA_toSubMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (P : ProjSubMeas Outcome 𝒜) (a0 : Outcome) :
                  (completeAtOutcomeProjA hM P a0).toSubMeas = (Preliminaries.completeAtOutcome P.toSubMeas a0).toSubMeas

                  The submeasurement of completeAtOutcomeProjA hM P a0 is that of completeAtOutcome.

                  source
                  theorem MIPRE.LIDT.Co.ProjMeas.isPVMIn_of_isFinitePair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (Q : ProjMeas Outcome 𝒜) :
                  IsPVMIn Q.outcome

                  A projective measurement of the first player's algebra of a finite pair is a projective measurement of the repository (MIPRE.IsPVMIn): Co ProjMeas.isPVMIn in the commutant IsFinitePair.equivA identifies 𝒜 with, pulled back along isPVMIn_map_equiv_iff.

                  source
                  noncomputable def MIPRE.LIDT.Co.TwoSpace.completeAtOutcomeProjB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder ℬ] [StarOrderedRing ℬ] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (P : ProjSubMeas Outcome ℬ) (a0 : Outcome) :
                  ProjMeas Outcome ℬ

                  Complete a projective submeasurement of the second player's algebra of a finite pair at a distinguished outcome, through IsFinitePair.equivB.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem MIPRE.LIDT.Co.TwoSpace.completeAtOutcomeProjB_toMeasurement {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder ℬ] [StarOrderedRing ℬ] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (P : ProjSubMeas Outcome ℬ) (a0 : Outcome) :
                    (completeAtOutcomeProjB hM P a0).toMeasurement = Preliminaries.completeAtOutcome P.toSubMeas a0

                    The measurement of completeAtOutcomeProjB hM P a0 is the canonical completion completeAtOutcome P.toSubMeas a0 in ℬ.

                    source
                    theorem MIPRE.LIDT.Co.TwoSpace.completeAtOutcomeProjB_toSubMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder ℬ] [StarOrderedRing ℬ] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (P : ProjSubMeas Outcome ℬ) (a0 : Outcome) :
                    (completeAtOutcomeProjB hM P a0).toSubMeas = (Preliminaries.completeAtOutcome P.toSubMeas a0).toSubMeas

                    The submeasurement of completeAtOutcomeProjB hM P a0 is that of completeAtOutcome.

                    source
                    theorem MIPRE.LIDT.Co.ProjMeas.isPVMIn_of_isFinitePairB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder ℬ] [StarOrderedRing ℬ] (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (Q : ProjMeas Outcome ℬ) :
                    IsPVMIn Q.outcome

                    A projective measurement of the second player's algebra of a finite pair is a projective measurement of the repository, through IsFinitePair.equivB.