Finite attained correlated minimax value and saddle point

Open

QAlgorithms.Papers.Independent.Intakethird100.P80.theorem2

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For a fixed finite quantum experiment $Q$ , use the full setting simplex $\Sigma$ and the full local-theory simplex $\Pi$ . Put $U(\sigma,\pi)=D_2(Q_\sigma\|P_{\sigma;\pi})$ . There are $0\le V<\infty$ , $\sigma^*\in\Sigma$ , and $\pi^*\in\Pi$ such that

\inf_{\pi\in\Pi}\sup_{\sigma\in\Sigma}U(\sigma,\pi)=V=\sup_{\sigma\in\Sigma}\inf_{\pi\in\Pi}U(\sigma,\pi),

both outer extrema are attained at the displayed strategies, and for every $\sigma\in\Sigma$ and $\pi\in\Pi$ ,

U(\sigma,\pi^*)\le U(\sigma^*,\pi^*)=V\le U(\sigma^*,\pi).

This supplies an actual saddle point for potentially correlated settings. The minimizer inequality agrees with both the display in Definition 4 on PDF p.13 and the proof on p.35; the supplied plan incorrectly described the displayed inequality as reversed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P80

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P80

open scoped BigOperators ENNReal Topology Classical

open MeasureTheory Filter

/-- PDF p.14, Theorem 2; proof p.35: finite correlated value, both attainments,
and both saddle inequalities (matching the source display on p.13). -/
theorem theorem2 {S : BellExperiment} (Q : Table S) (hQ : NonlocalityProof Q) :
    ∃ V : ℝ≥0∞, 0 ≤ V ∧ V < ⊤ ∧
      minimax Q (stdSimplex ℝ (Settings S)) = V ∧ correlatedStrength Q = V ∧
      ∃ (s : Sigma S) (p : PiLocal S),
        upperValue Q (stdSimplex ℝ (Settings S)) p.1 = V ∧ lowerValue Q s.1 = V ∧
        statisticalPayoff Q s.1 p.1 = V ∧ Saddle Q (stdSimplex ℝ (Settings S)) s.1 p.1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P80

end

Source

The statistical strength of nonlocality proofs, arXiv:quant-ph/0307125v2, PDF p. 14, Theorem 2: finite attained correlated minimax value

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $S$ be any Bell experiment with a positive number of parties and positive finite numbers of settings and outcomes at each applicable party and setting. Let $\Omega$ be its setting tuples, $X_a$ its outcome tuples at setting $a$ , and $\mathcal V$ its assignments $v_i(b)$ of an outcome to every setting of every party. Write $\Delta(E)$ for the nonnegative real functions on a finite set $E$ summing to $1$ . Let $Q_a(x)$ be a real table whose rows are probability distributions, whose marginal probabilities on every subset of parties agree whenever the settings on that subset agree, and for which there exist positive local dimensions, a positive semidefinite joint matrix $\rho$ of trace $1$ , and positive semidefinite local measurement matrices $M_{i,b,u}$ summing to the identity over $u$ , such that $Q_a(x)=\operatorname{Re}\operatorname{tr}((\bigotimes_i M_{i,a_i,x_i})\rho)$ . For $p\in\Delta(\mathcal V)$ , put $P_p(a,x)=\sum_{v:\,v_i(a_i)=x_i\ \forall i}p(v)$ . For finite probability distributions $q,r$ , define $D(q\Vert r)$ to be $\infty$ if $q(z)>0=r(z)$ for some $z$ , and otherwise to be the extended nonnegative number $\max\{0,\sum_{z:q(z)\ne0}q(z)\log_2(q(z)/r(z))\}$ . Set

D_s(p)=D((s(a)Q_a(x))_{a,x}\Vert(s(a)P_p(a,x))_{a,x}), \qquad F(s)=\inf_{r\in\Delta(\mathcal V)}D_s(r), \qquad U(p)=\sup_{t\in\Delta(\Omega)}D_t(p).

Then there exist an extended nonnegative real $V$ with $0\le V<\infty$ , a distribution $s\in\Delta(\Omega)$ , and a distribution $p\in\Delta(\mathcal V)$ , such that

\inf_{r\in\Delta(\mathcal V)}U(r) =\sup_{t\in\Delta(\Omega)}F(t) =U(p)=F(s)=D_s(p)=V,

and, for every $t\in\Delta(\Omega)$ and $r\in\Delta(\mathcal V)$ ,

D_t(p)\le D_s(p)\le D_s(r).

The setting and potential distributions may have zero coordinates, and the finite value $V$ is allowed to be $0$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph