Bridge, part 5, over models: consistency defects of complete measurements

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

Generic facts about the port's two-space bipartite consistency defect qBipartiteConsDefect M A B = max 0 (bornProb (A_tot, B_tot) − ∑ₐ bornProb (A_a, B_a)) (Co/Test/StrategyBiProj/Measurements.lean), over a bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ with star-ordered algebras, when the measurements A, B are complete (total = 1) and the state is a unit vector (‖M.ψ‖ = 1):

• the defect is 1 − ∑ₐ bornProb (A_a, B_a) (qBipartiteConsDefect_of_complete), and equals the off-diagonal mass ∑_{a ≠ b} bornProb (A_a, B_b) (qBipartiteConsDefect_eq_offDiagonal);
• for coarse-grainings postprocess A f, postprocess B g, the matching mass is ∑_{a, b : f a = g b} bornProb (A_a, B_b) (qBipartiteMatchMass_postprocess), so the defect is bounded by 1 − acc whenever acc is a sum of some of the terms bornProb (A_a, B_b) with f a = g b (qBipartiteConsDefect_postprocess_le).

The translation is the matrix bridge's with ev ψ (opTensor X Y) read as M.bornProb X Y and the normalization ψ.IsNormalized as ‖M.ψ‖ = 1; the sums of Born probabilities go through M.bornProb_sum_left and M.bornProb_sum_right. These are the facts through which the value of a strategy (Co/Bridge/Value.lean) is compared with the port's failure surrogate.

Not ported

Every declaration of the matrix bridge is redeclared here under its name, for a bipartite model: ev_opTensor_outcome_nonneg and sum_ev_opTensor_outcome (stated with M.bornProb), qBipartiteMatchMass_postprocess, qBipartiteMatchMass_le_one, qBipartiteConsDefect_of_complete, qBipartiteConsDefect_eq_offDiagonal, qBipartiteConsDefect_postprocess_le and bipartiteConsError_uniform. Nothing is left out.

theorem MIPRE.LIDT.Co.Bridge.ev_opTensor_outcome_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (A : SubMeas α 𝒜) (B : SubMeas β ℬ) (a : α) (b : β) : 0 ≤ M.bornProb (A.outcome a) (B.outcome b)

Born probabilities of pairs of measurement operators are nonnegative.

theorem MIPRE.LIDT.Co.Bridge.sum_ev_opTensor_outcome {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (hψ : ‖M.ψ‖ = 1) (A : SubMeas α 𝒜) (B : SubMeas β ℬ) (hA : A.total = 1) (hB : B.total = 1) : ∑ a : α, ∑ b : β, M.bornProb (A.outcome a) (B.outcome b) = 1

The Born probabilities of two complete measurements on a unit vector sum to one.

theorem MIPRE.LIDT.Co.Bridge.qBipartiteMatchMass_postprocess {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {γ : Type u_6} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq γ] (A : SubMeas α 𝒜) (B : SubMeas β ℬ) (f : α → γ) (g : β → γ) : qBipartiteMatchMass M (postprocess A f) (postprocess B g) = ∑ a : α, ∑ b : β, if f a = g b then M.bornProb (A.outcome a) (B.outcome b) else 0

The matching mass of two coarse-grained measurements.

theorem MIPRE.LIDT.Co.Bridge.qBipartiteMatchMass_le_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} [Fintype α] (hψ : ‖M.ψ‖ = 1) (A : SubMeas α 𝒜) (B : SubMeas α ℬ) (hA : A.total = 1) (hB : B.total = 1) : qBipartiteMatchMass M A B ≤ 1

The matching mass of two complete measurements on a unit vector is at most one.

theorem MIPRE.LIDT.Co.Bridge.qBipartiteConsDefect_of_complete {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} [Fintype α] (hψ : ‖M.ψ‖ = 1) (A : SubMeas α 𝒜) (B : SubMeas α ℬ) (hA : A.total = 1) (hB : B.total = 1) : qBipartiteConsDefect M A B = 1 - qBipartiteMatchMass M A B

For complete measurements on a unit vector the defect is 1 − matching mass.

theorem MIPRE.LIDT.Co.Bridge.qBipartiteConsDefect_eq_offDiagonal {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} [Fintype α] [DecidableEq α] (hψ : ‖M.ψ‖ = 1) (A : SubMeas α 𝒜) (B : SubMeas α ℬ) (hA : A.total = 1) (hB : B.total = 1) : qBipartiteConsDefect M A B = ∑ a : α, ∑ b : α, if a = b then 0 else M.bornProb (A.outcome a) (B.outcome b)

For complete measurements on a unit vector the defect is the off-diagonal mass.

theorem MIPRE.LIDT.Co.Bridge.qBipartiteConsDefect_postprocess_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {γ : Type u_6} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq γ] (hψ : ‖M.ψ‖ = 1) (A : SubMeas α 𝒜) (B : SubMeas β ℬ) (hA : A.total = 1) (hB : B.total = 1) (f : α → γ) (g : β → γ) (D : α → β → Prop) [DecidableRel D] (hD : ∀ (a : α) (b : β), D a b → f a = g b) : qBipartiteConsDefect M (postprocess A f) (postprocess B g) ≤ 1 - ∑ a : α, ∑ b : β, if D a b then M.bornProb (A.outcome a) (B.outcome b) else 0

The defect of two coarse-grainings of complete measurements on a unit vector is at most 1 − acc for any acceptance mass acc made of terms that force equal coarse-grained outcomes.

Averages over uniform distributions

theorem MIPRE.LIDT.Co.Bridge.bipartiteConsError_uniform {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} [Fintype α] {X : Type u_7} [Fintype X] [DecidableEq X] [Nonempty X] (A : IdxSubMeas X α 𝒜) (B : IdxSubMeas X α ℬ) : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution X) A B = 1 / ↑(Fintype.card X) * ∑ x : X, qBipartiteConsDefect M (A x) (B x)

The consistency error under the uniform distribution is the average of the defects.