Documentation

MIPRE.Background.LIDT.Co.Basic.MeasurementLift

Measurement lift infrastructure for the low individual degree test #

Measurement-level tensor-factor lifts built from the submeasurement placement API: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/MeasurementLift.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The vendored lifts are Kronecker placements, with completeness from leftTensor_one. Here a measurement on the local algebra 𝔓 is placed on a factor by Measurement.map along the ⋆-homomorphism S.L or S.R of a symmetric model S (Co/Basic/SubMeasurementCore.lean), whose completeness is map_one. As with S.leftPlacedSubMeas, the lifts are SymModel declarations used with dot notation, the model replacing the vendored named carriers (ιA := ιA), (ιB := ιB).

New here #

leftLiftedMeasurement_toSubMeas, leftLiftedMeasurement_outcome and their right counterparts, the projection equations of the lifts (all rfl).

Not ported #

Every declaration of the vendored file has a counterpart here.

source
noncomputable def MIPRE.LIDT.Co.SymModel.leftLiftedMeasurement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : Measurement α 𝔓) :
Measurement α (K →L[ℂ] K)

Lift a measurement to the first tensor factor: each outcome A_a becomes S.L A_a.

Equations
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.SymModel.rightLiftedMeasurement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : Measurement α 𝔓) :
    Measurement α (K →L[ℂ] K)

    Lift a measurement to the second tensor factor: each outcome A_a becomes S.R A_a.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LIDT.Co.SymModel.leftLiftedMeasurement_toSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : Measurement α 𝔓) :
      (S.leftLiftedMeasurement A).toSubMeas = S.leftPlacedSubMeas A.toSubMeas

      The underlying submeasurement of a left-lifted measurement is the left placement.

      source
      @[simp]
      theorem MIPRE.LIDT.Co.SymModel.leftLiftedMeasurement_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : Measurement α 𝔓) (a : α) :
      (S.leftLiftedMeasurement A).outcome a = S.L (A.outcome a)

      Outcome operators of a left-lifted measurement are left placements.

      source
      @[simp]
      theorem MIPRE.LIDT.Co.SymModel.rightLiftedMeasurement_toSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : Measurement α 𝔓) :
      (S.rightLiftedMeasurement A).toSubMeas = S.rightPlacedSubMeas A.toSubMeas

      The underlying submeasurement of a right-lifted measurement is the right placement.

      source
      @[simp]
      theorem MIPRE.LIDT.Co.SymModel.rightLiftedMeasurement_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : Measurement α 𝔓) (a : α) :
      (S.rightLiftedMeasurement A).outcome a = S.R (A.outcome a)

      Outcome operators of a right-lifted measurement are right placements.