Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.MakingMeasurementsProjective.NaimarkCore

Section 5 — Naimark core #

Core projector and compression lemmas for the one-measurement Naimark dilation construction.

One-measurement Naimark (Lemma 5.2) #

source
theorem MIPStarRE.LDT.MakingMeasurementsProjective.optionBasisProj_isProj {α : Type u_1} [Fintype α] [DecidableEq α] (oa : Option α) :
Quantum.IsProj (Matrix.single oa oa 1)

The rank-one projector onto an Option basis vector is projective.

source
theorem MIPStarRE.LDT.MakingMeasurementsProjective.optionBasisProj_sum_eq_one {α : Type u_1} [Fintype α] [DecidableEq α] :
∑ oa : Option α, Matrix.single oa oa 1 = 1

The Option basis projectors sum to the identity.

source
theorem MIPStarRE.LDT.MakingMeasurementsProjective.isProj_kronecker {d₁ : Type u_1} {d₂ : Type u_2} [Fintype d₁] [Fintype d₂] {A : Quantum.Op d₁} {B : Quantum.Op d₂} (hA : Quantum.IsProj A) (hB : Quantum.IsProj B) :
Quantum.IsProj (Matrix.kronecker A B)

Kronecker products of projectors are projective.

source
theorem MIPStarRE.LDT.MakingMeasurementsProjective.isProj_unitary_conj {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) {P : Quantum.Op n} (hP : Quantum.IsProj P) :
Quantum.IsProj ((↑U).conjTranspose * P * ↑U)

Unitary conjugation preserves projectivity.

source
theorem MIPStarRE.LDT.MakingMeasurementsProjective.unitary_conj_sum_eq_one {β : Type u_1} {n : Type u_2} [Fintype β] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) (P : β → Quantum.Op n) (hP : ∑ b : β, P b = 1) :
∑ b : β, (↑U).conjTranspose * P b * ↑U = 1

Unitary conjugation preserves identity decompositions.

source
noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkRemainder {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (M : Quantum.Submeasurement α d) :
Quantum.Op d

The slack operator I - ∑_a M_a for one-measurement Naimark dilation.

Equations
Instances For
    source
    def MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkAuxTransition {α : Type u_1} [DecidableEq α] (oa ob : Option α) :
    Quantum.Op (Option α)

    The auxiliary matrix unit used in the one-measurement Naimark construction.

    Equations
    Instances For
      source
      noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkColumn {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (M : Quantum.Submeasurement α d) :
      Quantum.Op (d × Option α)

      The partial-isometry column implementing the one-measurement Naimark map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkInputProj {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] :
        Quantum.Op (d × Option α)

        The projector onto the input none slice of the auxiliary register.

        Equations
        Instances For
          source
          def MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkOutcomeProj {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (oa : Option α) :
          Quantum.Op (d × Option α)

          The auxiliary-basis projector for a given Naimark outcome slice.

          Equations
          Instances For
            source
            theorem MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkRemainder_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (M : Quantum.Submeasurement α d) :
            0 ≤ oneMeasNaimarkRemainder M

            The one-measurement Naimark slack operator is positive semidefinite.

            source
            theorem MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkOutcomeProj_mul_column {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (M : Quantum.Submeasurement α d) (a : α) :
            oneMeasNaimarkOutcomeProj (some a) * oneMeasNaimarkColumn M = (CFC.sqrt (M.effect a)).kronecker (Matrix.single (some a) none 1)

            Multiplying by an outcome projector isolates the matching square-root block of the Naimark column.

            source
            theorem MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkInputProj_isProj {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] :
            Quantum.IsProj oneMeasNaimarkInputProj

            The input-slice projector in the one-measurement Naimark dilation is projective.

            source
            theorem MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkColumn_isometry {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (M : Quantum.Submeasurement α d) :
            Matrix.conjTranspose (oneMeasNaimarkColumn M) * oneMeasNaimarkColumn M = oneMeasNaimarkInputProj

            Isometry property of the Naimark column: V†V = P.

            The Naimark column V satisfies V†V = I ⊗ |⊥⟩⟨⊥|, i.e., it is an isometry on the designated input slice of the auxiliary register. This is the key linear-algebraic content justifying the unitary extension.

            source
            theorem MIPStarRE.LDT.MakingMeasurementsProjective.oneMeasNaimarkCompression {α : Type u_1} [Fintype α] [DecidableEq α] {d : Type u_2} [Fintype d] [DecidableEq d] (M : Quantum.Submeasurement α d) (a : α) :
            Matrix.conjTranspose (oneMeasNaimarkColumn M) * oneMeasNaimarkOutcomeProj (some a) * oneMeasNaimarkColumn M = Matrix.kronecker (M.effect a) (naimarkAuxProjector α)

            Compressing the dilated outcome projector recovers the original effect.