Documentation

MIPRE.Foundations.Introspection.RegisterTransport

Transporting finite register operators and their state distances #

All transports below are explicit permutations of computational basis labels. In particular they preserve positivity, projectivity and squared state norms.

source
def MIPRE.Introspection.registerOp {I : Type u_1} {J : Type u_2} (e : I ≃ J) (M : Matrix J J ℂ) :
Matrix I I ℂ

Pull an operator back along a bijective labelling of the basis.

Equations
Instances For
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_apply {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M : Matrix J J ℂ) (i j : I) :
    registerOp e M i j = M (e i) (e j)
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_one {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) :
    registerOp e 1 = 1
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_sub {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M N : Matrix J J ℂ) :
    registerOp e (M - N) = registerOp e M - registerOp e N
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_mul {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M N : Matrix J J ℂ) :
    registerOp e (M * N) = registerOp e M * registerOp e N
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_sum {I : Type u_1} {J : Type u_2} {A : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] (e : I ≃ J) (M : A → Matrix J J ℂ) :
    registerOp e (∑ a : A, M a) = ∑ a : A, registerOp e (M a)
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_conjTranspose {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M : Matrix J J ℂ) :
    registerOp e M.conjTranspose = (registerOp e M).conjTranspose
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_symm {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M : Matrix I I ℂ) :
    registerOp e (registerOp e.symm M) = M
    source
    @[simp]
    theorem MIPRE.Introspection.registerOp_inv {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M : Matrix J J ℂ) :
    registerOp e.symm (registerOp e M) = M
    source
    theorem MIPRE.Introspection.registerOp_posSemidef {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) {M : Matrix J J ℂ} (hM : M.PosSemidef) :
    (registerOp e M).PosSemidef

    Positivity is preserved without changing any eigenvalues.

    source
    theorem MIPRE.Introspection.registerOp_isPVM {I : Type u_1} {J : Type u_2} {A : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] (e : I ≃ J) {M : A → Matrix J J ℂ} (hM : IsPVM M) :
    IsPVM fun (a : A) => registerOp e (M a)

    A projective measurement remains projective after permuting its basis.

    source
    def MIPRE.Introspection.registerPOVM {I : Type u_1} {J : Type u_2} {A : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] (e : I ≃ J) (M : POVM A J) :
    POVM A I

    Transport the actual normalized positive measurement, rather than only its matrices.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Introspection.registerPOVM_mats {I : Type u_1} {J : Type u_2} {A : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] (e : I ≃ J) (M : POVM A J) (a : A) :
      ↑((registerPOVM e M).mats a) = registerOp e ↑(M.mats a)
      source
      theorem MIPRE.Introspection.norm_evec_comp_equiv {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (v : J → ℂ) :
      ‖evec (v ∘ ⇑e)‖ = ‖evec v‖

      A computational-basis permutation preserves the Euclidean norm.

      source
      theorem MIPRE.Introspection.registerOp_mulVec {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (M : Matrix J J ℂ) (v : J → ℂ) :
      (registerOp e M).mulVec (v ∘ ⇑e) = M.mulVec v ∘ ⇑e

      Simultaneous matrix and vector reindexing commutes with matrix application.

      source
      theorem MIPRE.Introspection.registerOp_kronecker {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K] [Fintype L] [DecidableEq L] (e : I ≃ J) (f : K ≃ L) (M : Matrix J J ℂ) (N : Matrix L L ℂ) :
      registerOp (e.prodCongr f) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (registerOp e M) (registerOp f N)
      source
      theorem MIPRE.Introspection.stateSqNorm_registerOp {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K] [Fintype L] [DecidableEq L] (e : I ≃ J) (f : K ≃ L) (ψ : J × L → ℂ) (M : Matrix J J ℂ) :
      stateSqNorm (ψ ∘ ⇑(e.prodCongr f)) (registerOp e M) = stateSqNorm ψ M

      State distances are unchanged by independent permutations of the two parties.