Documentation

MIPRE.Foundations.Expanded

The expanded state, and an inert ancilla #

The expansion stage of the Pauli appendix (sec:expanding) adjoins a maximally entangled pair of ancilla registers to each player and then re-bipartitions: Alice's party becomes her own register together with her half of the ancilla, and Bob's becomes his register together with the other half. This file is that construction, for an arbitrary ancilla state.

The one thing it has to support #

Every statement of the expansion stage is a norm on the expanded state, and the operators that appear are of the form M (x) N --- the strategy's own operator on the original register, the ancilla's on the adjoined one. Two facts carry all of them:

Together they say that an operator with an inert ancilla, M (x) Id, has the same state-norm on the expanded state as M has on the original one, provided the ancilla state is a unit vector (norm_stateVec_expVec_kron_one). That is what lets a bound proved before the expansion be used after it, which is how the expansion stage consumes lem:qld-obs-commutation.

In a bipartite model #

The construction itself is the ancilla extension BipartiteModel.expand of any bipartite model (MIPRE/Foundations/AncillaModel.lean), and the expanded state is its instance at the tensor-product model: bornProb_expVec_eq identifies the Born probabilities of product operators, after which the norm of the expanded state, the inert ancilla and the factorization of Born probabilities are the model's (norm_expand_state, stateSqNorm_expand_smulKron_one, bornProb_expand_smulKron), and the product of projective measurements is IsPVMIn.smulKron read through kronEquiv. What stays here is the coordinate computation that a product operator acts on the product vector factor by factor (mulVec_kron_kron_expVec).

In a model #

Two facts of this file are not about the ancilla at all, and are proved once for a bipartite model: a unitary in front is invisible to the state norm, and a common coarse-graining of both players can only increase their agreement.

source
theorem MIPRE.BipartiteModel.stateNorm_mul_of_isometry {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (M : BipartiteModel ๐’ž ๐’œ โ„ฌ) {W : ๐’œ} (h : star W * W = 1) (N : ๐’œ) :
M.stateNorm (W * N) = M.stateNorm N

A unitary in front is invisible to the state norm.

source
theorem MIPRE.BipartiteModel.bornProb_sum_sum {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (M : BipartiteModel ๐’ž ๐’œ โ„ฌ) {ฮน : Type u_4} (s t : Finset ฮน) (a : ฮน โ†’ ๐’œ) (b : ฮน โ†’ โ„ฌ) :
M.bornProb (โˆ‘ i โˆˆ s, a i) (โˆ‘ j โˆˆ t, b j) = โˆ‘ i โˆˆ s, โˆ‘ j โˆˆ t, M.bornProb (a i) (b j)
source
theorem MIPRE.BipartiteModel.sum_bornProb_le_map {๐’ž : 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 ฮน] [DecidableEq ฮน] [Fintype ฮบ] [DecidableEq ฮบ] (P : POVMIn ฮน ๐’œ) (Q : POVMIn ฮน โ„ฌ) (f : ฮน โ†’ ฮบ) :
โˆ‘ i : ฮน, M.bornProb (P.op i) (Q.op i) โ‰ค โˆ‘ k : ฮบ, M.bornProb ((POVMIn.map f P).op k) ((POVMIn.map f Q).op k)

Coarse-graining both players the same way can only increase agreement: the terms the coarse-graining adds are Born probabilities of positive elements.

source
def MIPRE.expVec {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) :
(dA ร— anc) ร— dB ร— anc' โ†’ โ„‚

The expanded state: the strategy's state on the original registers, tensored with an ancilla state whose two halves go to the two different parties.

Equations
Instances For
    source
    def MIPRE.expEquiv (dA : Type u_5) (dB : Type u_6) (anc : Type u_7) (anc' : Type u_8) :
    (dA ร— anc) ร— dB ร— anc' โ‰ƒ (dA ร— dB) ร— anc ร— anc'

    The reindexing that separates the two systems from the two parties.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.sum_prod_mul {X : Type u_5} {Y : Type u_6} {M : Type u_7} [Fintype X] [Fintype Y] [CommRing M] (f : X โ†’ M) (g : Y โ†’ M) :
      โˆ‘ q : X ร— Y, f q.1 * g q.2 = (โˆ‘ x : X, f x) * โˆ‘ y : Y, g y

      A product of sums as a sum over the product.

      Product operators on the expanded state, in coordinates #

      source
      theorem MIPRE.expVec_dotProduct_of_pair {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (u u' : dA ร— dB โ†’ โ„‚) (v v' : anc ร— anc' โ†’ โ„‚) :
      star (expVec u v) โฌแตฅ expVec u' v' = star u โฌแตฅ u' * star v โฌแตฅ v'
      source
      theorem MIPRE.mulVec_kron_kron_expVec {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) (X : Matrix dA dA โ„‚) (Y : Matrix anc anc โ„‚) (X' : Matrix dB dB โ„‚) (Y' : Matrix anc' anc' โ„‚) :
      (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X Y) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X' Y')).mulVec (expVec ฯˆ e) = expVec ((Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X X').mulVec ฯˆ) ((Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) Y Y').mulVec e)

      An operator of product form on each party acts factor by factor.

      source
      theorem MIPRE.mulVec_kron_expVec {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) (M : Matrix dA dA โ„‚) (N : Matrix anc anc โ„‚) :
      (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) M N) 1).mulVec (expVec ฯˆ e) = expVec ((Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) M 1).mulVec ฯˆ) ((Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) N 1).mulVec e)

      An operator of product form acts on the expanded state factor by factor.

      source
      theorem MIPRE.swapVec_expVec {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) :
      swapVec (expVec ฯˆ e) = expVec (swapVec ฯˆ) (swapVec e)

      Exchanging the two parties of the expanded state exchanges both factors.

      The expanded state is the ancilla extension of the tensor-product model #

      source
      theorem MIPRE.bornProb_expVec_eq {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) (X : Matrix dA dA โ„‚) (Y : Matrix anc anc โ„‚) (X' : Matrix dB dB โ„‚) (Y' : Matrix anc' anc' โ„‚) :
      bornProb (expVec ฯˆ e) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X Y) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X' Y') = ((BipartiteModel.tensor ฯˆ).expand e).bornProb (smulKron X Y) (smulKron X' Y')

      The bridge: a product measurement's Born probability on the expanded state is its Born probability in the ancilla extension of the tensor-product model.

      source
      theorem MIPRE.norm_evec_expVec {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (u : dA ร— dB โ†’ โ„‚) (v : anc ร— anc' โ†’ โ„‚) :
      โ€–evec (expVec u v)โ€– = โ€–evec uโ€– * โ€–evec vโ€–

      The norm of a product state is the product of the norms: norm_expand_state at the tensor-product model.

      source
      theorem MIPRE.expVec_dotProduct {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) :
      star (expVec ฯˆ e) โฌแตฅ expVec ฯˆ e = star ฯˆ โฌแตฅ ฯˆ * star e โฌแตฅ e

      The expanded state's norm splits, so it is a unit vector when both factors are.

      source
      theorem MIPRE.expVec_unit {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] {ฯˆ : dA ร— dB โ†’ โ„‚} {e : anc ร— anc' โ†’ โ„‚} (hฯˆ : star ฯˆ โฌแตฅ ฯˆ = 1) (he : star e โฌแตฅ e = 1) :
      star (expVec ฯˆ e) โฌแตฅ expVec ฯˆ e = 1
      source
      theorem MIPRE.norm_stateVec_kron_unitary {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (v : (dA ร— anc) ร— dB ร— anc' โ†’ โ„‚) (D : Matrix dA dA โ„‚) {U : Matrix anc anc โ„‚} (hU : U.conjTranspose * U = 1) :
      โ€–stateVec v (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) D U)โ€– = โ€–stateVec v (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) D 1)โ€–

      A unitary on the ancilla is invisible to the state-norm. D (x) U = (Id (x) U)(D (x) Id) and the front factor is unitary on the whole space (stateNorm_mul_of_isometry).

      source
      theorem MIPRE.stateSqNorm_expVec_kron_one {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) (M : Matrix dA dA โ„‚) :
      stateSqNorm (expVec ฯˆ e) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) M 1) = ((BipartiteModel.tensor ฯˆ).expand e).stateSqNorm (smulKron M 1)

      The first player's operator with an inert ancilla, on the expanded state, is the ancilla extension's M โŠ— 1.

      source
      theorem MIPRE.norm_stateVec_expVec_kron_one {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) {e : anc ร— anc' โ†’ โ„‚} (he : โ€–evec eโ€– = 1) (M : Matrix dA dA โ„‚) :
      โ€–stateVec (expVec ฯˆ e) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) M 1)โ€– = โ€–stateVec ฯˆ Mโ€–

      An inert ancilla changes nothing: a bound proved before the expansion survives it. This is stateSqNorm_expand_smulKron_one at the tensor-product model.

      Born probabilities on the expanded state #

      The expansion stage's consistency statements are about a measurement of product form, and what they need is that its Born probabilities factorize (bornProb_expand_smulKron).

      source
      theorem MIPRE.bornProb_expVec_kron {dA : Type u_1} {dB : Type u_2} {anc : Type u_3} {anc' : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype anc] [DecidableEq anc] [Fintype anc'] [DecidableEq anc'] (ฯˆ : dA ร— dB โ†’ โ„‚) (e : anc ร— anc' โ†’ โ„‚) {X : Matrix dA dA โ„‚} {Y : Matrix anc anc โ„‚} {X' : Matrix dB dB โ„‚} {Y' : Matrix anc' anc' โ„‚} (hY : Y.PosSemidef) (hY' : Y'.PosSemidef) :
      bornProb (expVec ฯˆ e) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X Y) (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X' Y') = bornProb ฯˆ X X' * bornProb e Y Y'

      The Born probability of a product measurement on the expanded state factorizes. Only the ancilla's two operators need to be positive: that is what makes their quadratic form real, which is what lets the real part of the product split.

      Data processing, at the Born level #

      The state-dependent distance has no data-processing inequality --- NW19 states theirs for the consistency distance and the remark following it gives a counterexample for approx. What is true, and what every coarse-graining in the appendix uses, is that applying the same post-processing to both players can only increase the probability that they agree. That is a statement about Born probabilities, and it is proved here so that no consumer is tempted by the other form.

      source
      theorem MIPRE.bornProb_sum_sum {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ฮน : Type u_5} (ฯˆ : dA ร— dB โ†’ โ„‚) (s t : Finset ฮน) (A : ฮน โ†’ Matrix dA dA โ„‚) (B : ฮน โ†’ Matrix dB dB โ„‚) :
      bornProb ฯˆ (โˆ‘ i โˆˆ s, A i) (โˆ‘ j โˆˆ t, B j) = โˆ‘ i โˆˆ s, โˆ‘ j โˆˆ t, bornProb ฯˆ (A i) (B j)
      source
      theorem MIPRE.sum_bornProb_le_map {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ฮน : Type u_5} {ฮบ : Type u_6} [Fintype ฮน] [DecidableEq ฮน] [Fintype ฮบ] [DecidableEq ฮบ] (ฯˆ : dA ร— dB โ†’ โ„‚) (P : POVM ฮน dA) (Q : POVM ฮน dB) (f : ฮน โ†’ ฮบ) :
      โˆ‘ i : ฮน, bornProb ฯˆ โ†‘(P.mats i) โ†‘(Q.mats i) โ‰ค โˆ‘ k : ฮบ, bornProb ฯˆ โ†‘((POVM.map f P).mats k) โ†‘((POVM.map f Q).mats k)

      Coarse-graining both players the same way can only increase agreement.

      The product measurement #

      source
      def MIPRE.POVM.kron {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] {ฮน : Type u_5} {ฮบ : Type u_6} [Fintype ฮน] [Fintype ฮบ] (P : POVM ฮน dA) (Q : POVM ฮบ anc) :
      POVM (ฮน ร— ฮบ) (dA ร— anc)

      The product of two POVMs, on the two systems of one party: outcomes the pairs, elements the Kronecker products.

      Equations
      Instances For
        source
        @[simp]
        theorem MIPRE.POVM.kron_mats {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] {ฮน : Type u_5} {ฮบ : Type u_6} [Fintype ฮน] [Fintype ฮบ] (P : POVM ฮน dA) (Q : POVM ฮบ anc) (p : ฮน ร— ฮบ) :
        โ†‘((P.kron Q).mats p) = Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) โ†‘(P.mats p.1) โ†‘(Q.mats p.2)
        source
        theorem MIPRE.POVM.kron_map {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] {ฮน : Type u_5} {ฮบ : Type u_6} {ฮน' : Type u_7} {ฮบ' : Type u_8} [Fintype ฮน] [DecidableEq ฮน] [Fintype ฮบ] [DecidableEq ฮบ] [Fintype ฮน'] [DecidableEq ฮน'] [Fintype ฮบ'] [DecidableEq ฮบ'] (P : POVM ฮน dA) (Q : POVM ฮบ anc) (f : ฮน โ†’ ฮน') (g : ฮบ โ†’ ฮบ') :
        (map f P).kron (map g Q) = map (fun (p : ฮน ร— ฮบ) => (f p.1, g p.2)) (P.kron Q)

        Relabelling the two factors is relabelling the product.

        Projectivity of the constructions #

        The expansion stage's measurements are products of a strategy measurement with an ancilla measurement, coarse-grained by adding the two outcomes, and the arguments downstream need them to be projective. Two closures give that: a product of projective measurements is projective, and so is any coarse-graining of one (IsPVM.coarse).

        source
        def MIPRE.kronEquiv {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] :
        Matrix anc anc (Matrix dA dA โ„‚) โ‰ƒโ‹†+* Matrix (dA ร— anc) (dA ร— anc) โ„‚

        The matrices over the first system's matrices, as matrices of the product of the first system with the register: the identification under which smulKron X P is X โŠ—โ‚– P.

        Equations
        Instances For
          source
          theorem MIPRE.kronEquiv_smulKron {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] (X : Matrix dA dA โ„‚) (P : Matrix anc anc โ„‚) :
          kronEquiv (smulKron X P) = Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) X P
          source
          theorem MIPRE.isPVM_kron {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] {ฮน : Type u_5} {ฮบ : Type u_6} [Fintype ฮน] [DecidableEq ฮน] [Fintype ฮบ] [DecidableEq ฮบ] {P : ฮน โ†’ Matrix dA dA โ„‚} {Q : ฮบ โ†’ Matrix anc anc โ„‚} (hP : IsPVM P) (hQ : IsPVM Q) :
          IsPVM fun (p : ฮน ร— ฮบ) => Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) (P p.1) (Q p.2)

          A product of projective measurements is projective: IsPVMIn.smulKron, read through kronEquiv.

          source
          theorem MIPRE.isPVM_povm_map {dA : Type u_1} [Fintype dA] [DecidableEq dA] {A : Type u_5} {B : Type u_6} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (M : POVM A dA) (h : IsPVM fun (a : A) => โ†‘(M.mats a)) (f : A โ†’ B) :
          IsPVM fun (b : B) => โ†‘((POVM.map f M).mats b)

          A coarse-graining of a projective POVM is projective, in the POVM.map form the games use.

          source
          theorem MIPRE.isPVM_povm_kron {dA : Type u_1} {anc : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype anc] [DecidableEq anc] {ฮน : Type u_5} {ฮบ : Type u_6} [Fintype ฮน] [DecidableEq ฮน] [Fintype ฮบ] [DecidableEq ฮบ] (P : POVM ฮน dA) (Q : POVM ฮบ anc) (hP : IsPVM fun (i : ฮน) => โ†‘(P.mats i)) (hQ : IsPVM fun (j : ฮบ) => โ†‘(Q.mats j)) :
          IsPVM fun (p : ฮน ร— ฮบ) => โ†‘((P.kron Q).mats p)

          A product of projective POVMs is projective, in the POVM.kron form the expansion uses.