Lemma 14 (G4): convexity of Suc

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.product_strength_convex

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

prove2quantum

All Bell scenarios have independent finite, nonempty Alice and Bob input and output alphabets. A behavior is a nonnegative conditional output law normalized at every input pair; $\mathrm{NS}$ imposes both no-signaling marginal identities. Processing uses one initial box with rules and randomness fixed independently of the supplied behavior. Write $D(P\Vert Q)$ for classical Kullback–Leibler divergence with natural logarithms, zero numerator contributing zero and positive numerator over zero contributing $+\infty$ . Define $S_b(P\Vert Q)=\max_{x,y}D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ . For an input law $d$ , put $D_d(P\Vert Q)=\sum_{x,y}d(x,y)D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ , with zero-weight terms equal to zero. Let $\mathcal L$ be all local-hidden-variable behaviors on the same alphabets. Define $S_{\rm nl}(P)=\min_{Q\in\mathcal L}S_b(P\Vert Q)$ , $S_u(P)=\min_{Q\in\mathcal L}D_u(P\Vert Q)$ for the uniform joint law $u$ , $S_{uc}(P)=\max_{d_X,d_Y}\min_{Q\in\mathcal L}D_{d_Xd_Y}(P\Vert Q)$ , and $S_c(P)=\max_d\min_{Q\in\mathcal L}D_d(P\Vert Q)$ over all joint laws. For $P,Q\in\mathrm{NS}$ on the same scenario and every real $0\le\mu\le1$ ,

S_{uc}(\mu P+(1-\mu)Q)\le\mu S_{uc}(P)+(1-\mu)S_{uc}(Q).

This is convexity in the behavior. The product-input maximum remains outside the local minimum; no minimax over the nonconvex set of product laws is asserted.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P29

Formal statement

noncomputable section

open scoped BigOperators ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P29

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Advance50.P47
  (Box IsCorrelation IsNoSignaling HasLocalModel TwoLocalBoxes losrTransform
   correlationMixture)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Dependency50.P47 (Law)

/-- PDF p.15, Lemma 14, (G4). Convexity in the behavior, with the product-law
maximum still outside the local minimum; no product-law minimax is used. -/
theorem product_strength_convex {s : BellScenario}
    (p q : Behavior s) (hp : IsNS p) (hq : IsNS q)
    (mu : ℝ) (hmu0 : 0 ≤ mu) (hmu1 : mu ≤ 1) :
    suc (correlationMixture p q mu) ≤
      ENNReal.ofReal mu * suc p + ENNReal.ofReal (1 - mu) * suc q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 15, Lemma 14 (G4)

Read-back

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

Let $s$ be any Bell scenario with finite nonempty question sets $X,Y$ and answer sets $A,B$ . Let $p,q$ be nonnegative arrays normalized over $A\times B$ at every question pair, and assume both have Bob’s marginal independent of Alice’s question and Alice’s marginal independent of Bob’s question. Let $\mathcal L_s$ consist of all such normalized nonnegative arrays admitting a local representation $\ell(x,y,a,b)=\sum_h\pi(h)A_h(a\mid x)B_h(b\mid y)$ , where the hidden-variable set is arbitrary, $\pi$ is a discrete probability mass function, and the response distributions are nonnegative and normalized. For finite probability arrays $r,v$ , set $D(r\|v)=+\infty$ if some $r_i>0$ has $v_i=0$ , and otherwise set $D(r\|v)=\max\{0,\sum_i r_i\log(r_i/v_i)\}$ , using natural logarithms and total real division and logarithm at zero. Define

S_{\mathrm{prod}}(r)= \sup_{\substack{d_X\ge0,\ \sum_xd_X(x)=1\\d_Y\ge0,\ \sum_yd_Y(y)=1}} \inf_{\ell\in\mathcal L_s} \sum_{x,y}d_X(x)d_Y(y)\, D\bigl(r(x,y,\cdot,\cdot)\,\|\,\ell(x,y,\cdot,\cdot)\bigr).

For every real $\mu$ with $0\le\mu\le1$ , one has $S_{\mathrm{prod}}(\mu p+(1-\mu)q)\le\mu S_{\mathrm{prod}}(p)+(1-\mu)S_{\mathrm{prod}}(q)$ , where the mixture is pointwise. The endpoints $\mu=0,1$ and input distributions with zero entries are included; all expressions use extended nonnegative arithmetic, including $0\cdot(+\infty)=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