structure CommutingRepetition.CommutingStrategy (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type (u + 1)

A commuting-operator strategy over question alphabets X, Y and answer alphabets A, B: a complex Hilbert space H, a unit vector ψ, and POVM families E x (Alice) and F y (Bob) of positive continuous linear maps summing to 1, with every Alice effect commuting with every Bob effect. [02_preliminaries.tex; audit def commuting_strategy]

• H : Type u
• normedAddCommGroup : NormedAddCommGroup self.H
• innerProductSpace : InnerProductSpace ℂ self.H
• completeSpace : CompleteSpace self.H
• ψ : self.H
• ψ_norm : ‖self.ψ‖ = 1
• E : X → A → self.H →L[ℂ] self.H
• F : Y → B → self.H →L[ℂ] self.H
• E_pos (x : X) (a : A) : (self.E x a).IsPositive
• F_pos (y : Y) (b : B) : (self.F y b).IsPositive
• E_sum (x : X) : ∑ a : A, self.E x a = 1
• F_sum (y : Y) : ∑ b : B, self.F y b = 1
• commutes (x : X) (y : Y) (a : A) (b : B) : Commute (self.E x a) (self.F y b)

noncomputable def CommutingRepetition.CommutingStrategy.correlation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : ℝ

The correlation table of a strategy: p(a, b | x, y) = ⟪ψ, E_x^a F_y^b ψ⟫ (a real number; the inner product is real because the commuting product of self-adjoint effects is self-adjoint). [02_preliminaries.tex, success-probability display]

Equations

• S.correlation x y a b = (inner ℂ S.ψ ((S.E x a) ((S.F y b) S.ψ))).re

theorem CommutingRepetition.CommutingStrategy.jointEffect_isPositive {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : (S.E x a ∘SL S.F y b).IsPositive

Each Alice–Bob joint effect is a positive operator: a commuting product of positive operators is positive (Commute.mul_nonneg, via the continuous functional calculus on H →L[ℂ] H and the Loewner order).

theorem CommutingRepetition.CommutingStrategy.correlation_inner_im_eq_zero {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : (inner ℂ S.ψ ((S.E x a) ((S.F y b) S.ψ))).im = 0

The correlation's defining inner product is real: E_x^a F_y^b is symmetric (commuting product of positive operators), so ⟪ψ, EFψ⟫ equals its own conjugate. Certifies that the .re in correlation is lossless (DIFFERENCES.md D7).

theorem CommutingRepetition.CommutingStrategy.correlation_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : 0 ≤ S.correlation x y a b

theorem CommutingRepetition.CommutingStrategy.correlation_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) : ∑ a : A, ∑ b : B, S.correlation x y a b = 1

Completeness: for every question pair the answers exhaust the state: ∑_{a,b} p(a,b|x,y) = 1.

theorem CommutingRepetition.CommutingStrategy.correlation_le_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : S.correlation x y a b ≤ 1

noncomputable def CommutingRepetition.CommutingStrategy.trivial {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] : CommutingStrategy X Y A B

The trivial strategy on H = ℂ: answers a fixed pair deterministically. Witnesses nonemptiness of the strategy space.

Equations

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