Bridge, part 3: measurements

A strategy for our game carries one projective measurement per question, with outcomes in Answer F m d. The MIPStarRE strategy container ProjStrat 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.

This file builds these from the strategy's measurements at the canonical line questions: the measurement at a presentation ℓ is the coarse-graining (ProjMeas.postprocess) 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 ℓ, where s = b + c·t is the change of parameters. Covariance under rebasing then follows from the composition law affine_comp_shift, and ill-typed answers are sent to the zero polynomial.

Lemmas on canonical lines

theorem MIPRE.LIDT.Line.find_congr {m : ℕ} {p q : Fin m → Prop} [DecidablePred p] [DecidablePred q] (hp : ∃ (k : Fin m), p k) (hq : ∃ (k : Fin m), q k) (h : ∀ (k : Fin m), p k ↔ q k) : Fin.find p hp = Fin.find q hq

Fin.find only depends on the predicate.

theorem MIPRE.LIDT.Line.through_add_smul {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (u v : Point F m) (t : F) : through (u + t • v) v = through u v

The canonical presentation only depends on the line.

theorem MIPRE.LIDT.Line.mem_through {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (u v : Point F m) : (through u v).Mem u

The base point of a canonical presentation lies on it.

theorem MIPRE.LIDT.Line.param_through {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (u v : Point F m) : (through u v).param u = if h : ∃ (j : Fin m), v j ≠ 0 then u (Fin.find (fun (j : Fin m) => v j ≠ 0) h) else 0

The parameter of the base point on its canonical presentation.

theorem MIPRE.LIDT.Line.param_through_single {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (u : Point F m) (i : Fin m) : (through u (Pi.single i 1)).param u = u i

The parameter of a point on its canonical axis-parallel line is its coordinate in the direction of the line.

From projective measurement families to MIPStarRE measurements

def MIPRE.LIDT.Bridge.toProjMeas {X : Type u_2} {A : Type u_3} {n : Type u_4} [Fintype A] [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) : MIPStarRE.LDT.ProjMeas A n

The measurement for the question x of a projective family on ℂ^{n×n}, as a MIPStarRE projective measurement.

Equations

• MIPRE.LIDT.Bridge.toProjMeas P x = { outcome := P.M x, total := 1, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯, total_eq_one := ⋯, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Bridge.toProjMeas_outcome {X : Type u_2} {A : Type u_3} {n : Type u_4} [Fintype A] [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) (a : A) : (toProjMeas P x).outcome a = P.M x a

@[simp]

theorem MIPRE.LIDT.Bridge.toProjMeas_total {X : Type u_2} {A : Type u_3} {n : Type u_4} [Fintype A] [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) : (toProjMeas P x).total = 1

theorem MIPRE.LIDT.Bridge.postprocess_outcome_congr {α : Type u_2} {β : Type u_3} {ι : Type u_4} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (M : MIPStarRE.LDT.ProjMeas α ι) (φ φ' : α → β) (b b' : β) (h : ∀ (a : α), φ' a = b' ↔ φ a = b) : (M.postprocess φ').outcome b' = (M.postprocess φ).outcome b

Two coarse-grainings of the same measurement agree on outcomes whose fibers agree.

Affine reparametrization of line answers

noncomputable def MIPRE.LIDT.Bridge.affine {F : Type u_1} [Field F] (g : Polynomial F) (b c : F) : Polynomial F

Substitute b + c·X into a univariate polynomial.

Equations

• MIPRE.LIDT.Bridge.affine g b c = g.comp (Polynomial.C b + Polynomial.C c * Polynomial.X)

theorem MIPRE.LIDT.Bridge.natDegree_affine_le {F : Type u_1} [Field F] {g : Polynomial F} {k : ℕ} (hg : g.natDegree ≤ k) (b c : F) : (affine g b c).natDegree ≤ k

theorem MIPRE.LIDT.Bridge.affine_comp_shift {F : Type u_1} [Field F] (g : Polynomial F) (b c t : F) : (affine g b c).comp (Polynomial.C t + Polynomial.X) = affine g (b + c * t) c

Shifting the parameter of an affinely reparametrized polynomial.

@[simp]

theorem MIPRE.LIDT.Bridge.eval_affine {F : Type u_1} [Field F] (g : Polynomial F) (b c t : F) : Polynomial.eval t (affine g b c) = Polynomial.eval (b + c * t) g

noncomputable def MIPRE.LIDT.Bridge.axisPolyOf {F : Type u_1} [Field F] {m d : ℕ} : Answer F m d → Polynomial F

The univariate polynomial of degree ≤ d answered to an axis-parallel line question (0 for ill-typed answers).

Equations

• MIPRE.LIDT.Bridge.axisPolyOf (MIPRE.LIDT.Answer.axisPoly c) = MIPRE.LIDT.Bridge.ofCoeffs c
• MIPRE.LIDT.Bridge.axisPolyOf x✝ = 0

theorem MIPRE.LIDT.Bridge.natDegree_axisPolyOf_le {F : Type u_1} [Field F] {m d : ℕ} (a : Answer F m d) : (axisPolyOf a).natDegree ≤ d

noncomputable def MIPRE.LIDT.Bridge.diagPolyOf {F : Type u_1} [Field F] {m d : ℕ} : Answer F m d → Polynomial F

The univariate polynomial of degree ≤ m·d answered to a diagonal line question (0 for ill-typed answers).

Equations

• MIPRE.LIDT.Bridge.diagPolyOf (MIPRE.LIDT.Answer.diagPoly c) = MIPRE.LIDT.Bridge.ofCoeffs c
• MIPRE.LIDT.Bridge.diagPolyOf x✝ = 0

theorem MIPRE.LIDT.Bridge.natDegree_diagPolyOf_le {F : Type u_1} [Field F] {m d : ℕ} (a : Answer F m d) : (diagPolyOf a).natDegree ≤ m * d

noncomputable def MIPRE.LIDT.Bridge.axisAnswer {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (b : F) (a : Answer F m d) : MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)

The axis-line answer, in the parameter t of a presentation whose base point has parameter b on the canonical line (so that s = b + t), read from an answer of the strategy at the canonical question.

Equations

• MIPRE.LIDT.Bridge.axisAnswer b a = { poly := MIPRE.LIDT.Bridge.affine (MIPRE.LIDT.Bridge.axisPolyOf a) b 1, degreeBounded := ⋯ }

noncomputable def MIPRE.LIDT.Bridge.diagAnswer {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (b c : F) (a : Answer F m d) : MIPStarRE.LDT.DiagonalLinePolynomial (lidtParams F m d)

The diagonal-line answer, in the parameter t of a presentation related to the canonical parameter by s = b + c·t, read from an answer of the strategy at the canonical question.

Equations

• MIPRE.LIDT.Bridge.diagAnswer b c a = { poly := MIPRE.LIDT.Bridge.affine (MIPRE.LIDT.Bridge.diagPolyOf a) b c, degreeBounded := ⋯ }

theorem MIPRE.LIDT.Bridge.axisAnswer_reparamAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (b : F) (a : Answer F m d) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : (axisAnswer b a).reparamAt t = axisAnswer (b + dec t) a

theorem MIPRE.LIDT.Bridge.diagAnswer_reparamAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (b c : F) (a : Answer F m d) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : (diagAnswer b c a).reparamAt t = diagAnswer (b + c * dec t) c a

theorem MIPRE.LIDT.Bridge.axisAnswer_zeroCoord {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (b : F) (a : Answer F m d) : (axisAnswer b a).toFun MIPStarRE.LDT.zeroCoord = enc (Polynomial.eval b (axisPolyOf a))

The value at the coded parameter 0 of an axis-line answer.

theorem MIPRE.LIDT.Bridge.diagAnswer_zeroCoord {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (b c : F) (a : Answer F m d) : (diagAnswer b c a).toFun MIPStarRE.LDT.zeroCoord = enc (Polynomial.eval b (diagPolyOf a))

The value at the coded parameter 0 of a diagonal-line answer.

Line measurement families

noncomputable def MIPRE.LIDT.Bridge.axisCanon {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.AxisParallelLine (lidtParams F m d)) : Line F m

The canonical line of an axis-parallel line presentation.

Equations

• MIPRE.LIDT.Bridge.axisCanon ℓ = MIPRE.LIDT.Line.through (MIPRE.LIDT.Bridge.decP ℓ.base) (Pi.single ℓ.direction 1)

noncomputable def MIPRE.LIDT.Bridge.axisBase {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.AxisParallelLine (lidtParams F m d)) : F

The parameter, on the canonical line, of the base point of an axis-parallel line presentation.

Equations

• MIPRE.LIDT.Bridge.axisBase ℓ = MIPRE.LIDT.Bridge.dec (ℓ.base ℓ.direction)

noncomputable def MIPRE.LIDT.Bridge.axisMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement (Question F m) (Answer F m d) (Matrix n n ℂ)) : MIPStarRE.LDT.IdxProjMeas (MIPStarRE.LDT.AxisParallelLine (lidtParams F m d)) (MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)) n

The axis-parallel line measurement family induced by a strategy's measurement family.

Equations

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

theorem MIPRE.LIDT.Bridge.axisCanon_rebaseAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.AxisParallelLine (lidtParams F m d)) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : axisCanon (ℓ.rebaseAt t) = axisCanon ℓ

theorem MIPRE.LIDT.Bridge.axisBase_rebaseAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.AxisParallelLine (lidtParams F m d)) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : axisBase (ℓ.rebaseAt t) = axisBase ℓ + dec t

theorem MIPRE.LIDT.Bridge.axisMeas_invariant {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement (Question F m) (Answer F m d) (Matrix n n ℂ)) : MIPStarRE.LDT.AxisParallelMeasurementReparamInvariant (lidtParams F m d) (axisMeas P)

noncomputable def MIPRE.LIDT.Bridge.diagCanon {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d)) : Line F m

The canonical line of a diagonal line presentation.

Equations

• MIPRE.LIDT.Bridge.diagCanon ℓ = MIPRE.LIDT.Line.through (MIPRE.LIDT.Bridge.decP ℓ.base) (MIPRE.LIDT.Bridge.decP ℓ.direction)

noncomputable def MIPRE.LIDT.Bridge.diagData {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d)) : F × F

The change of parameters s = b + c·t from a diagonal line presentation to its canonical line: b is the pivot coordinate of the base point and c the pivot coordinate of the direction ((0, 0) for a singleton line).

Equations

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

noncomputable def MIPRE.LIDT.Bridge.diagMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement (Question F m) (Answer F m d) (Matrix n n ℂ)) : MIPStarRE.LDT.IdxProjMeas (MIPStarRE.LDT.DiagonalLine (lidtParams F m d)) (MIPStarRE.LDT.DiagonalLinePolynomial (lidtParams F m d)) n

The diagonal line measurement family induced by a strategy's measurement family.

Equations

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

theorem MIPRE.LIDT.Bridge.diagCanon_rebaseAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d)) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : diagCanon (ℓ.rebaseAt t) = diagCanon ℓ

theorem MIPRE.LIDT.Bridge.diagData_rebaseAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d)) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : diagData (ℓ.rebaseAt t) = ((diagData ℓ).1 + (diagData ℓ).2 * dec t, (diagData ℓ).2)

theorem MIPRE.LIDT.Bridge.diagMeas_invariant {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement (Question F m) (Answer F m d) (Matrix n n ℂ)) : MIPStarRE.LDT.DiagonalMeasurementReparamInvariant (lidtParams F m d) (diagMeas P)

Point measurement families

noncomputable def MIPRE.LIDT.Bridge.codedValue {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (a : Answer F m d) : MIPStarRE.LDT.Fq (lidtParams F m d)

The coded value of an answer to a point question.

Equations

• MIPRE.LIDT.Bridge.codedValue a = MIPRE.LIDT.Bridge.enc a.toValue

noncomputable def MIPRE.LIDT.Bridge.pointMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement (Question F m) (Answer F m d) (Matrix n n ℂ)) : MIPStarRE.LDT.IdxProjMeas (MIPStarRE.LDT.Point (lidtParams F m d)) (MIPStarRE.LDT.Fq (lidtParams F m d)) n

The point measurement family induced by a strategy's measurement family.

Equations

• MIPRE.LIDT.Bridge.pointMeas P u = (MIPRE.LIDT.Bridge.toProjMeas P (MIPRE.LIDT.Question.point (MIPRE.LIDT.Bridge.decP u))).postprocess MIPRE.LIDT.Bridge.codedValue