noncomputable def CommutingRepetition.PreroundedStrategy.samplingError {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) : ℝ

The π-averaged unhalved ℓ¹ sampling error of a resource against the ideal pair law — the quantity the sampling theorem controls by C_OT (Δ^{1/6} + ξ). [07_main_theorem.tex, eq main-OT-error]

Equations

• P.samplingError R = ∑ h : P.Hist, ∑ x : X, ∑ y : Y, P.Q h x y * ∑ a : A, ∑ b : B, |R.answerLaw (h, x) (h, y) a b - P.idealCorrelation (h, x) (h, y) a b|

theorem CommutingRepetition.PreroundedStrategy.samplingError_eq_labelLaw {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) : P.samplingError R = ∑ s : P.Hist × X, ∑ t : P.Hist × Y, P.labelLaw s t * ∑ a : A, ∑ b : B, |R.answerLaw s t a b - P.idealCorrelation s t a b|

The sampling error is the π-average of the ℓ¹ answer-law error — the exact quantity otqcs_sampling controls.

noncomputable def CommutingRepetition.PreroundedStrategy.tuplePayoff {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) (t : P.Hist × X × Y) : ℝ

The actual expected payoff on a tuple, when the two locally generated histories agree: F(h, x, y) = ∑_{a,b} V(a,b|x,y) q̂_{(h,x),(h,y)}(a,b), defined for every tuple including tuples outside the support of Q. [07_main_theorem.tex, display defining F]

Equations

• P.tuplePayoff G R t = ∑ a : A, ∑ b : B, G.payoff t.2.1 t.2.2 a b * R.answerLaw (t.1, t.2.1) (t.1, t.2.2) a b

theorem CommutingRepetition.PreroundedStrategy.tuplePayoff_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) (t : P.Hist × X × Y) : 0 ≤ P.tuplePayoff G R t

theorem CommutingRepetition.PreroundedStrategy.tuplePayoff_le_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) (t : P.Hist × X × Y) : P.tuplePayoff G R t ≤ 1

theorem CommutingRepetition.abs_expectation_sub_le_totalVariation {ι : Type u_1} [Fintype ι] {p q F : ι → ℝ} (hp_nonneg : ∀ (i : ι), 0 ≤ p i) (hp_sum : ∑ i : ι, p i = 1) (hq_nonneg : ∀ (i : ι), 0 ≤ q i) (hq_sum : ∑ i : ι, q i = 1) (hF0 : ∀ (i : ι), 0 ≤ F i) (hF1 : ∀ (i : ι), F i ≤ 1) : |∑ i : ι, p i * F i - ∑ i : ι, q i * F i| ≤ Pinsker.finiteTotalVariation p q

Change of measure by total variation (node 1.4.3, generic form; 07_main_theorem.tex, eq payoff-under-JA): for laws p, q and a [0,1]- valued observable, expectations differ by at most the (halved) total variation.

theorem CommutingRepetition.PreroundedStrategy.payoff_under_ideal {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) : P.idealSuccess G - P.samplingError R / 2 ≤ ∑ t : P.Hist × X × Y, P.Qflat t * P.tuplePayoff G R t

Payoff under the ideal law (node 1.4.2; 07_main_theorem.tex, eq payoff-under-Q): an unhalved ℓ¹ answer-law error changes the [0,1]-valued expected payoff by at most half that error, so E_Q F ≥ idealSuccess − samplingError/2.

theorem CommutingRepetition.one_shot_strategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (G : Game X Y A B) (P : PreroundedStrategy X Y A B) (R : SamplingResource (P.Hist × X) (P.Hist × Y) A B) : ∃ (Sc : CommutingStrategy X Y A B), P.idealSuccess G - P.samplingError R / 2 - Pinsker.finiteTotalVariation P.Qflat (P.JAflat G) - P.mismatchProb G ≤ G.win Sc.correlation

The legal one-shot strategy and its payoff (nodes 1.4, 1.4.1, 1.4.4; 07_main_theorem.tex sec 7.2, eq one-shot-final-payoff): tensoring the sampling resource with the classical flag — seed ω ∼ ν, locally computed histories r_A(ω, x), r_B(ω, y), labels s = (r_A, x), t = (r_B, y) — yields a legal commuting strategy for G (state fixed before the questions, labels locally computable, Alice left, Bob right, all cross-commutators vanishing) with winning probability at least idealSuccess − samplingError/2 − d_TV(Q, J_A) − Pr[r_A ≠ r_B]. On the event r_A = r_B the conditional payoff is exactly the tuple payoff; on the complement it is nonnegative. The argument uses only the exact J_A marginal, one change of measure, and the mismatch probability.