Bridge, part 3, over models: measurements

The model counterpart of the repository's matrix bridge MIPRE/Background/LIDT/Bridge/Measurement.lean (not a vendored file; it serves the tensor instance and stays), in the port of planning/c6b-plan.md (milestone M14, unit M14-0).

A projective strategy for our game in a bipartite model carries one projective measurement per question, P : Question F m → POVMIn (Answer F m d) R with hP : ∀ x, IsPVMIn (P x).op, in a star-ordered ⋆-ring R (one of the two algebras of the model). The ported two-space strategy container MIPRE.LIDT.Co.ProjStrat (Co/Test/StrategyCore.lean) wants instead

• point measurements with outcomes in the coded field,
• a measurement for every presentation (base, direction) of an axis-parallel line, with outcomes the polynomials of degree ≤ d in the parameter of that presentation, covariant under rebasing the presentation (AxisParallelMeasurementReparamInvariant),
• and likewise for diagonal lines.

They are built as in the matrix bridge, from the strategy's measurements at the canonical line questions: the measurement at a presentation ℓ is the coarse-graining of the measurement at the canonical question of ℓ along the map sending an answer g (a polynomial in the canonical parameter s) to the polynomial t ↦ g(b + c·t) in the parameter t of ℓ. Covariance follows from the composition law affine_comp_shift, through the classical lemmas axisAnswer_reparamAt, axisCanon_rebaseAt, axisBase_rebaseAt and their diagonal analogues.

The coarse-graining. The port's ProjMeas.postprocess (Co/Basic/SubMeasurementFamilies.lean) asks for a C⋆-algebra, since it derives the orthogonality of the outcomes of a projective measurement from positivity. The algebras of a bipartite model in MIPRE.LIDT.Simul.SoundIn are only star-ordered ⋆-rings, so here the coarse-graining is postprocessMeas P hP x φ: the port's postprocess of the submeasurement toProjMeas P hP x, made projective by IsPVMIn.coarse, which uses the orthogonality that IsPVMIn records. In a C⋆-algebra it is ProjMeas.postprocess, by rfl (postprocessMeas_eq_postprocess).

Reused by import. Every classical declaration of the matrix bridge, which does not mention a measurement, is imported, not restated: the canonical-line lemmas Line.* (namespace MIPRE.LIDT.Line), affine and affine_comp_shift, the answer readings axisPolyOf, diagPolyOf, axisAnswer, diagAnswer with their *_reparamAt and *_zeroCoord lemmas, the canonical presentations axisCanon, axisBase, diagCanon, diagData with their *_rebaseAt lemmas, and codedValue. Those this file uses are named through an explicit open MIPRE.LIDT.Bridge (…) list, which names none of the declarations redeclared here.

Not ported

The declarations of the matrix bridge that mention a measurement are redeclared here, under their names, for an IsPVMIn family in a star-ordered ⋆-ring: toProjMeas, toProjMeas_outcome, toProjMeas_total, postprocess_outcome_congr (stated for the port's postprocess of any submeasurement), axisMeas, axisMeas_invariant, diagMeas, diagMeas_invariant and pointMeas. Nothing of the matrix bridge is left out; its classical half is imported, as above.

New here

• postprocessMeas, postprocessMeas_toSubMeas, postprocessMeas_outcome, postprocessMeas_eq_postprocess: the coarse-graining of an IsPVMIn family, above.

From projective families to the port's measurements

def MIPRE.LIDT.Co.Bridge.toProjMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) : ProjMeas A R

The measurement for the question x of a projective family P in R, as a projective measurement of the port (ProjMeas.ofIsPVMIn).

Equations

• MIPRE.LIDT.Co.Bridge.toProjMeas P hP x = MIPRE.LIDT.Co.ProjMeas.ofIsPVMIn (P x).op ⋯

@[simp]

theorem MIPRE.LIDT.Co.Bridge.toProjMeas_outcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) (a : A) : (toProjMeas P hP x).outcome a = (P x).op a

The outcomes of toProjMeas P hP x are those of P x.

@[simp]

theorem MIPRE.LIDT.Co.Bridge.toProjMeas_total {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) : (toProjMeas P hP x).total = 1

The total operator of toProjMeas P hP x is 1.

noncomputable def MIPRE.LIDT.Co.Bridge.postprocessMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) {B : Type u_4} [Fintype B] (φ : A → B) : ProjMeas B R

The coarse-graining of toProjMeas P hP x along φ: the port's postprocess of its submeasurement, projective by IsPVMIn.coarse. In a C⋆-algebra it is ProjMeas.postprocess (postprocessMeas_eq_postprocess).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LIDT.Co.Bridge.postprocessMeas_toSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) {B : Type u_4} [Fintype B] (φ : A → B) : (postprocessMeas P hP x φ).toSubMeas = postprocess (toProjMeas P hP x).toSubMeas φ

The submeasurement of postprocessMeas P hP x φ is the port's postprocess.

theorem MIPRE.LIDT.Co.Bridge.postprocessMeas_outcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) {B' : Type u_4} [Fintype B'] [DecidableEq B'] (φ : A → B') (b : B') : (postprocessMeas P hP x φ).outcome b = ∑ a : A with φ a = b, (P x).op a

The outcome of postprocessMeas P hP x φ at b is the sum of P x over the fibre of φ.

theorem MIPRE.LIDT.Co.Bridge.postprocess_outcome_congr {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (M : SubMeas α R) (φ φ' : α → β) (b b' : β) (h : ∀ (a : α), φ' a = b' ↔ φ a = b) : (postprocess M φ').outcome b' = (postprocess M φ).outcome b

Two coarse-grainings of the same submeasurement agree on outcomes whose fibres agree.

theorem MIPRE.LIDT.Co.Bridge.postprocessMeas_eq_postprocess {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {A : Type u_3} [Fintype A] (P : X → POVMIn A R) (hP : ∀ (x : X), IsPVMIn (P x).op) (x : X) {B : Type u_4} [Fintype B] (φ : A → B) : postprocessMeas P hP x φ = (toProjMeas P hP x).postprocess φ

In a C⋆-algebra, postprocessMeas is the port's ProjMeas.postprocess.

Line and point measurement families

noncomputable def MIPRE.LIDT.Co.Bridge.axisMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : Question F m → POVMIn (Answer F m d) R) (hP : ∀ (x : Question F m), IsPVMIn (P x).op) : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine (Bridge.lidtParams F m d)) (MIPStarRE.LDT.AxisLinePolynomial (Bridge.lidtParams F m d)) R

The axis-parallel line measurement family induced by a projective family P: at a presentation ℓ, the measurement at the canonical line of ℓ, its answers read in the parameter of ℓ.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.Bridge.axisMeas_invariant {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : Question F m → POVMIn (Answer F m d) R) (hP : ∀ (x : Question F m), IsPVMIn (P x).op) : AxisParallelMeasurementReparamInvariant (Bridge.lidtParams F m d) (axisMeas P hP)

The axis-parallel line measurement family induced by a projective family is covariant under rebasing.

noncomputable def MIPRE.LIDT.Co.Bridge.diagMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : Question F m → POVMIn (Answer F m d) R) (hP : ∀ (x : Question F m), IsPVMIn (P x).op) : IdxProjMeas (MIPStarRE.LDT.DiagonalLine (Bridge.lidtParams F m d)) (MIPStarRE.LDT.DiagonalLinePolynomial (Bridge.lidtParams F m d)) R

The diagonal line measurement family induced by a projective family P: at a presentation ℓ, the measurement at the canonical line of ℓ, its answers read in the parameter of ℓ through the change of parameters diagData ℓ.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.Bridge.diagMeas_invariant {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : Question F m → POVMIn (Answer F m d) R) (hP : ∀ (x : Question F m), IsPVMIn (P x).op) : DiagonalMeasurementReparamInvariant (Bridge.lidtParams F m d) (diagMeas P hP)

The diagonal line measurement family induced by a projective family is covariant under rebasing.

noncomputable def MIPRE.LIDT.Co.Bridge.pointMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : Question F m → POVMIn (Answer F m d) R) (hP : ∀ (x : Question F m), IsPVMIn (P x).op) : IdxProjMeas (MIPStarRE.LDT.Point (Bridge.lidtParams F m d)) (MIPStarRE.LDT.Fq (Bridge.lidtParams F m d)) R

The point measurement family induced by a projective family P: at a coded point u, the measurement at the point question decP u, its answers read as coded values.

Equations

• MIPRE.LIDT.Co.Bridge.pointMeas P hP u = MIPRE.LIDT.Co.Bridge.postprocessMeas P hP (MIPRE.LIDT.Question.point (MIPRE.LIDT.Bridge.decP u)) MIPRE.LIDT.Bridge.codedValue