Uniform averages and two order facts, shared by stages 4 and 5

The analysis of the Pauli basis test averages over uniform points and over the verifier's content, and compares Born probabilities of nonnegative operators. The few facts of that kind that both stage 4 (lem:qld-global-dummy, -products, -linear, -separate, -complete) and stage 5 (lem:qld-helper and after) use are collected here, so that stage 5 depends on stage 4 only through the interface MIPRE/Background/QLD/Simul.lean:

• the uniform weights are nonnegative and sum to one (uniform_nonneg, sum_uniform_eq_one);
• the uniform content, read through its two points, is a pair of independent uniform points (QLD.sum_content_blocks);
• the Born probability is monotone in the second player's operator when the first player's is nonnegative (bornProb_mono_right), and a self-adjoint idempotent is nonnegative (posSemidef_of_proj).

Stated in a bipartite model

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The two order facts were statements about matrices with the Loewner order (Matrix.PosSemidef); here they are stated in a bipartite model and in a star-ordered ring, whose order is the one generated by the elements z⋆ z (StarOrderedRing). The two combinatorial facts are unchanged.

Uniform weights

theorem MIPRE.sum_uniform_eq_one (X : Type u_1) [Fintype X] [Nonempty X] : ∑ x : X, uniform X x = 1

The uniform weights sum to one.

theorem MIPRE.uniform_nonneg (X : Type u_1) [Fintype X] (x : X) : 0 ≤ uniform X x

The uniform weights are nonnegative.

Two order facts

theorem MIPRE.posSemidef_of_proj {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {P : R} (hsa : star P = P) (hidem : P * P = P) : 0 ≤ P

A self-adjoint idempotent is nonnegative, in a star-ordered ring: it is P⋆ P.

theorem MIPRE.bornProb_mono_right {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : 𝒜} (hX : 0 ≤ X) {Y Y' : ℬ} (h : Y ≤ Y') : M.bornProb X Y ≤ M.bornProb X Y'

The Born probability is monotone in the second player's operator when the first player's is nonnegative.

The verifier's content, read through its two points

theorem MIPRE.QLD.sum_content_blocks {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} [NeZero m] (g : LIDT.Point F m → LIDT.Point F m → ℝ) : ∑ c : Content F m, (↑(Fintype.card (Content F m)))⁻¹ * g c.uX c.uZ = ∑ x : LIDT.Point F m, ∑ z : LIDT.Point F m, uniform (LIDT.Point F m) x * uniform (LIDT.Point F m) z * g x z

The uniform content, read through (uX, uZ), is a pair of independent uniform points.