Documentation

MIPRE.Background.LIDT.Co.Bridge.Strategy

Bridge, part 4, over models: strategies #

The model counterpart of the repository's matrix bridge MIPRE/Background/LIDT/Bridge/Strategy.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 M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ (S : M.ProjStrat (lidtGame F m d), MIPRE/Foundations/ModelStrategy.lean) is packaged as the port's two-space projective strategy MIPRE.LIDT.Co.ProjStrat (lidtParams F m d) 𝒞 𝒜 ℬ (Co/Test/StrategyCore.lean): the state is M itself, normalized by S.ψ_unit, and the six measurement families are those of Co/Bridge/Measurement.lean for S.PA in 𝒜 and S.PB in ℬ, with their four covariance fields. The rfl and coarse-graining equations at the end are the ones the value bridge reads the strategy through: point measurements as coded values of the point answers, and line measurements evaluated at the coded parameter 0 as the canonical line answers evaluated at the base point.

Not ported #

Of the matrix bridge, nonempty_of_unit, its Nonempty (Fin S.dA × Fin S.dB) instance, pureState and ev_toProjStrat are not carried over: they turn the state vector of a tensor-product strategy into a MIPStarRE density matrix, while the port's strategy takes the bipartite model M and its unit vector as they are. toProjStrat is toCoProjStrat here, and the equations pointMeasA_eq, pointMeasB_eq, axisMeasA_zero_eq, axisMeasB_zero_eq and diagMeas_zero_eq of the matrix Bridge/Value.lean are stated here, under their names, for toCoProjStrat.

source
noncomputable def MIPRE.LIDT.Co.Bridge.toCoProjStrat {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (lidtGame F m d)) :
ProjStrat (Bridge.lidtParams F m d) 𝒞 𝒜 ℬ

The port's two-space projective strategy induced by a projective strategy for our game in the bipartite model M: the state is M, and the measurement families are the point, axis-line and diagonal-line families of S.PA and S.PB.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.LIDT.Co.Bridge.toCoProjStrat_state {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (lidtGame F m d)) :
    (toCoProjStrat S).state = M

    The state of the induced strategy is the model.

    source
    theorem MIPRE.LIDT.Co.Bridge.pointMeasB_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (lidtGame F m d)) (u : MIPStarRE.LDT.Point (Bridge.lidtParams F m d)) :
    ((toCoProjStrat S).pointMeasurementB u).toSubMeas = postprocess (toProjMeas S.PB ⋯ (Question.point (Bridge.decP u))).toSubMeas Bridge.codedValue

    The point measurement of player B at a coded point, in coarse-grained form.

    source
    theorem MIPRE.LIDT.Co.Bridge.pointMeasA_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (lidtGame F m d)) (u : MIPStarRE.LDT.Point (Bridge.lidtParams F m d)) :
    ((toCoProjStrat S).pointMeasurementA u).toSubMeas = postprocess (toProjMeas S.PA ⋯ (Question.point (Bridge.decP u))).toSubMeas Bridge.codedValue

    The point measurement of player A at a coded point, in coarse-grained form.

    source
    theorem MIPRE.LIDT.Co.Bridge.axisMeasA_zero_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (lidtGame F m d)) (u : MIPStarRE.LDT.Point (Bridge.lidtParams F m d)) (i : Fin m) :
    (postprocess ((toCoProjStrat S).axisParallelMeasurementA { base := u, direction := i }).toSubMeas fun (x : MIPStarRE.LDT.AxisLinePolynomial (Bridge.lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) = postprocess (toProjMeas S.PA ⋯ (Question.axisLine (Line.through (Bridge.decP u) (Pi.single i 1)))).toSubMeas fun (a : Answer F m d) => Bridge.enc (Polynomial.eval (Bridge.decP u i) (Bridge.axisPolyOf a))

    The axis-parallel line measurement of player A evaluated at the coded parameter 0, in coarse-grained form: the canonical line answer evaluated at the base point.

    source
    theorem MIPRE.LIDT.Co.Bridge.axisMeasB_zero_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (lidtGame F m d)) (u : MIPStarRE.LDT.Point (Bridge.lidtParams F m d)) (i : Fin m) :
    (postprocess ((toCoProjStrat S).axisParallelMeasurementB { base := u, direction := i }).toSubMeas fun (x : MIPStarRE.LDT.AxisLinePolynomial (Bridge.lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) = postprocess (toProjMeas S.PB ⋯ (Question.axisLine (Line.through (Bridge.decP u) (Pi.single i 1)))).toSubMeas fun (a : Answer F m d) => Bridge.enc (Polynomial.eval (Bridge.decP u i) (Bridge.axisPolyOf a))

    The axis-parallel line measurement of player B evaluated at the coded parameter 0, in coarse-grained form.

    source
    theorem MIPRE.LIDT.Co.Bridge.diagMeas_zero_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {R : Type u_5} [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) (ℓ : MIPStarRE.LDT.DiagonalLine (Bridge.lidtParams F m d)) :
    (postprocess (diagMeas P hP ℓ).toSubMeas fun (x : MIPStarRE.LDT.DiagonalLinePolynomial (Bridge.lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) = postprocess (toProjMeas P hP (Question.diagLine (Line.through (Bridge.decP ℓ.base) (Bridge.decP ℓ.direction)))).toSubMeas fun (a : Answer F m d) => Bridge.enc (Polynomial.eval ((Line.through (Bridge.decP ℓ.base) (Bridge.decP ℓ.direction)).param (Bridge.decP ℓ.base)) (Bridge.diagPolyOf a))

    The diagonal line measurement of a projective family evaluated at the coded parameter 0, in coarse-grained form: the canonical line answer is read at the parameter of the base point.