The chained Bell walk: no-signalling plus chained correlations forces a uniform marginal

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #23.

A two-party outcome law is a function P : X → Y → O → O → ℝ, where P x y i j is the probability that Alice reads i at setting x while Bob reads j at setting y. Two outcomes o, oc are singled out, so the law is a two-outcome box (huniv, hoc below say that O is exactly {o, oc}). No-signalling is marginal invariance: Alice's marginal does not depend on Bob's setting, and conversely. That is the predicate CSD.SigmaLayer.HasNoSignalling, which lives in a higher layer of this repository and cannot be imported here, so it appears below as its two conjuncts hA and hB rather than as a second definition of the same thing.

The mathematics is one observation used twice. For a single pair of settings, two marginals of the same joint distribution differ by at most the probability that the two outcomes disagree (abs_marginalA_sub_marginalB_le), and they add to at most 1 plus the probability that the two outcomes agree (abs_marginalA_add_marginalB_sub_one_le). No-signalling is what lets those one-pair statements be chained across different pairs, because it makes each wing's marginal a function of that wing's setting alone.

• marginalA, marginalB, agree, disagree, chainCost;
• ★ abs_marginalA_sub_marginalB_le, ★ abs_marginalA_add_marginalB_sub_one_le — the two one-pair links;
• ★★ abs_marginalA_sub_marginalB_chain_le — the walk: along the alternating chain A 0, B 0, A 1, B 1, …, A n, B n the two end marginals differ by at most the sum of the 2n + 1 link disagreements;
• ★★★ abs_marginalA_sub_half_le — chained uniformity: closing the walk with an anticorrelated link between A 0 and B n forces Alice's marginal at A 0 to within (chainCost + agree (A 0) (B n)) / 2 of 1 / 2. Correlations around a chain that close up with one reversal leave no room for a biased marginal;
• ★★★ integral_abs_marginalA_sub_half_le — the same bound for every component of a mixture: if each q ξ is a no-signalling law and the mixture over ξ reproduces Q, then the components' marginals are 1 / 2 up to the bound computed from Q, in mean over ξ. The functional is affine in the law, so the components inherit the bound the mixture satisfies;
• ★ exists_signalling_of_sharp_integral — the contrapositive: a mixture whose components sharpen the marginal past that bound has a component that signals.

Honest scope

⚠️ Two outcomes and one distinguished pair of them. Nothing here is about more outcomes, more parties, or the chained inequality of Braunstein and Caves (a bound on a sum of correlations for local models), which is a neighbour of this walk and is not proved here.

⚠️ The bound is what it says: a bound. It is informative only when the chain's disagreements and the closing agreement are small, which is a property of the law the theorem is applied to, and for the quantum singlet that is Empirical/QM/ColbeckRenner.lean.

⚠️ chainCost counts the links of an alternating walk with A on one wing and B on the other. The settings are arbitrary functions of ℕ; no geometry is assumed here.

References: S. L. Braunstein, C. M. Caves, Wringing out better Bell inequalities, Ann. Phys. 202 (1990) 22 (the chained family); J. Barrett, L. Hardy, A. Kent, PRL 95 (2005) 010503 (the chained walk as a device-independent tool); R. Colbeck, R. Renner, No extension of quantum theory can have improved predictive power, Nat. Commun. 2 (2011) 411 (the use made of it in Empirical/QM/ColbeckRenner.lean); specs/colbeck-renner-note.md; specs/BACKLOG.md #23; specs/future-work.md.

Marginals, agreement, and the two one-pair links

def ProbabilityTheory.ChainedBell.marginalA {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] (P : X → Y → O → O → ℝ) (x : X) (y : Y) (i : O) : ℝ

Alice's marginal: the probability that she reads i at setting x, when Bob measures y.

Equations

• ProbabilityTheory.ChainedBell.marginalA P x y i = ∑ j : O, P x y i j

def ProbabilityTheory.ChainedBell.marginalB {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] (P : X → Y → O → O → ℝ) (x : X) (y : Y) (j : O) : ℝ

Bob's marginal: the probability that he reads j at setting y, when Alice measures x.

Equations

• ProbabilityTheory.ChainedBell.marginalB P x y j = ∑ i : O, P x y i j

def ProbabilityTheory.ChainedBell.agree {X : Type u_1} {Y : Type u_2} {O : Type u_3} (P : X → Y → O → O → ℝ) (o oc : O) (x : X) (y : Y) : ℝ

The probability that the two wings read the same outcome.

Equations

• ProbabilityTheory.ChainedBell.agree P o oc x y = P x y o o + P x y oc oc

def ProbabilityTheory.ChainedBell.disagree {X : Type u_1} {Y : Type u_2} {O : Type u_3} (P : X → Y → O → O → ℝ) (o oc : O) (x : X) (y : Y) : ℝ

The probability that the two wings read different outcomes.

Equations

• ProbabilityTheory.ChainedBell.disagree P o oc x y = P x y o oc + P x y oc o

theorem ProbabilityTheory.ChainedBell.sum_two {O : Type u_3} [Fintype O] [DecidableEq O] {o oc : O} {M : Type u_4} [AddCommMonoid M] (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (f : O → M) : ∑ i : O, f i = f o + f oc

A sum over a two-element outcome type is a two-term sum.

theorem ProbabilityTheory.ChainedBell.marginalA_eq {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} {x : X} {y : Y} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (i : O) : marginalA P x y i = P x y i o + P x y i oc

Alice's marginal, as a two-term sum.

theorem ProbabilityTheory.ChainedBell.marginalB_eq {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} {x : X} {y : Y} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (j : O) : marginalB P x y j = P x y o j + P x y oc j

Bob's marginal, as a two-term sum.

theorem ProbabilityTheory.ChainedBell.sum_eq_four {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} {x : X} {y : Y} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) : ∑ i : O, ∑ j : O, P x y i j = P x y o o + P x y o oc + (P x y oc o + P x y oc oc)

The normalisation of a two-outcome law, as a four-term identity.

theorem ProbabilityTheory.ChainedBell.agree_add_disagree_eq_one {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} {x : X} {y : Y} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hsum : ∑ i : O, ∑ j : O, P x y i j = 1) : agree P o oc x y + disagree P o oc x y = 1

Agreement and disagreement partition the normalisation.

theorem ProbabilityTheory.ChainedBell.abs_marginalA_sub_marginalB_le {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} {x : X} {y : Y} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hnn : ∀ (i j : O), 0 ≤ P x y i j) (i : O) : |marginalA P x y i - marginalB P x y i| ≤ disagree P o oc x y

★ The correlated link. Two marginals of one joint distribution differ by at most the probability that the outcomes disagree.

theorem ProbabilityTheory.ChainedBell.abs_marginalA_add_marginalB_sub_one_le {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} {x : X} {y : Y} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hnn : ∀ (i j : O), 0 ≤ P x y i j) (hsum : ∑ i : O, ∑ j : O, P x y i j = 1) (i : O) : |marginalA P x y i + marginalB P x y i - 1| ≤ agree P o oc x y

★ The anticorrelated link. Two marginals of one joint distribution add to 1 up to the probability that the outcomes agree.

The chained walk

def ProbabilityTheory.ChainedBell.chainCost {X : Type u_1} {Y : Type u_2} {O : Type u_3} (P : X → Y → O → O → ℝ) (o oc : O) (A : ℕ → X) (B : ℕ → Y) (n : ℕ) : ℝ

The total disagreement along the alternating walk A 0, B 0, A 1, B 1, …, A n, B n: one term for each of its 2n + 1 links.

Equations

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

theorem ProbabilityTheory.ChainedBell.chainCost_succ {X : Type u_1} {Y : Type u_2} {O : Type u_3} (P : X → Y → O → O → ℝ) (o oc : O) (A : ℕ → X) (B : ℕ → Y) (n : ℕ) : chainCost P o oc A B (n + 1) = chainCost P o oc A B n + disagree P o oc (A (n + 1)) (B n) + disagree P o oc (A (n + 1)) (B (n + 1))

Extending the walk by one node pair adds its two links.

theorem ProbabilityTheory.ChainedBell.abs_marginalA_sub_marginalB_chain_le {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hnn : ∀ (x : X) (y : Y) (i j : O), 0 ≤ P x y i j) (hA : ∀ (x : X) (y y' : Y) (i : O), marginalA P x y i = marginalA P x y' i) (hB : ∀ (x x' : X) (y : Y) (j : O), marginalB P x y j = marginalB P x' y j) (A : ℕ → X) (B : ℕ → Y) (i : O) (n : ℕ) : |marginalA P (A 0) (B 0) i - marginalB P (A n) (B n) i| ≤ chainCost P o oc A B n

★★ The chained walk. For a no-signalling law, the marginal at one end of the alternating walk and the marginal at the other end differ by at most the walk's total disagreement. The hypotheses hA and hB are no-signalling: each wing's marginal is a function of that wing's setting alone, which is what allows one-pair links to be composed across different pairs.

theorem ProbabilityTheory.ChainedBell.abs_marginalA_sub_half_le {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {P : X → Y → O → O → ℝ} {o oc : O} (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hnn : ∀ (x : X) (y : Y) (i j : O), 0 ≤ P x y i j) (hsum : ∀ (x : X) (y : Y), ∑ i : O, ∑ j : O, P x y i j = 1) (hA : ∀ (x : X) (y y' : Y) (i : O), marginalA P x y i = marginalA P x y' i) (hB : ∀ (x x' : X) (y : Y) (j : O), marginalB P x y j = marginalB P x' y j) (A : ℕ → X) (B : ℕ → Y) (i : O) (n : ℕ) : |marginalA P (A 0) (B 0) i - 1 / 2| ≤ (chainCost P o oc A B n + agree P o oc (A 0) (B n)) / 2

★★★ Chained uniformity. Close the walk with an anticorrelated link between its two ends: then Alice's marginal at A 0 is within half the total of the walk's disagreements and the closing agreement of 1 / 2. A chain of correlations that closes up with one reversal leaves no room for a biased marginal.

Every component of a mixture inherits the bound

theorem ProbabilityTheory.ChainedBell.integrable_marginalA {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (x : X) (y : Y) (i : O) : MeasureTheory.Integrable (fun (ξ : Ξ) => marginalA (q ξ) x y i) μ

A marginal of a mixture component is integrable when the law's entries are.

theorem ProbabilityTheory.ChainedBell.integral_marginalA {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {Q : X → Y → O → O → ℝ} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (hmix : ∀ (x : X) (y : Y) (i j : O), ∫ (ξ : Ξ), q ξ x y i j ∂μ = Q x y i j) (x : X) (y : Y) (i : O) : ∫ (ξ : Ξ), marginalA (q ξ) x y i ∂μ = marginalA Q x y i

Mixing commutes with taking a marginal.

theorem ProbabilityTheory.ChainedBell.integrable_disagree {X : Type u_1} {Y : Type u_2} {O : Type u_3} {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {o oc : O} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (x : X) (y : Y) : MeasureTheory.Integrable (fun (ξ : Ξ) => disagree (q ξ) o oc x y) μ

Disagreement of a mixture component is integrable when the law's entries are.

theorem ProbabilityTheory.ChainedBell.integral_disagree {X : Type u_1} {Y : Type u_2} {O : Type u_3} {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {Q : X → Y → O → O → ℝ} {o oc : O} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (hmix : ∀ (x : X) (y : Y) (i j : O), ∫ (ξ : Ξ), q ξ x y i j ∂μ = Q x y i j) (x : X) (y : Y) : ∫ (ξ : Ξ), disagree (q ξ) o oc x y ∂μ = disagree Q o oc x y

Mixing commutes with disagreement.

theorem ProbabilityTheory.ChainedBell.integrable_agree {X : Type u_1} {Y : Type u_2} {O : Type u_3} {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {o oc : O} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (x : X) (y : Y) : MeasureTheory.Integrable (fun (ξ : Ξ) => agree (q ξ) o oc x y) μ

Agreement of a mixture component is integrable when the law's entries are.

theorem ProbabilityTheory.ChainedBell.integral_agree {X : Type u_1} {Y : Type u_2} {O : Type u_3} {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {Q : X → Y → O → O → ℝ} {o oc : O} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (hmix : ∀ (x : X) (y : Y) (i j : O), ∫ (ξ : Ξ), q ξ x y i j ∂μ = Q x y i j) (x : X) (y : Y) : ∫ (ξ : Ξ), agree (q ξ) o oc x y ∂μ = agree Q o oc x y

Mixing commutes with agreement.

theorem ProbabilityTheory.ChainedBell.integrable_chainCost {X : Type u_1} {Y : Type u_2} {O : Type u_3} {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {o oc : O} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (A : ℕ → X) (B : ℕ → Y) (n : ℕ) : MeasureTheory.Integrable (fun (ξ : Ξ) => chainCost (q ξ) o oc A B n) μ

The walk's cost for a mixture component is integrable when the law's entries are.

theorem ProbabilityTheory.ChainedBell.integral_chainCost {X : Type u_1} {Y : Type u_2} {O : Type u_3} {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {Q : X → Y → O → O → ℝ} {o oc : O} (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (hmix : ∀ (x : X) (y : Y) (i j : O), ∫ (ξ : Ξ), q ξ x y i j ∂μ = Q x y i j) (A : ℕ → X) (B : ℕ → Y) (n : ℕ) : ∫ (ξ : Ξ), chainCost (q ξ) o oc A B n ∂μ = chainCost Q o oc A B n

Mixing commutes with the walk's cost: the functional is affine in the law.

theorem ProbabilityTheory.ChainedBell.integral_abs_marginalA_sub_half_le {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {Q : X → Y → O → O → ℝ} {o oc : O} [MeasureTheory.IsProbabilityMeasure μ] (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hnn : ∀ (ξ : Ξ) (x : X) (y : Y) (i j : O), 0 ≤ q ξ x y i j) (hsum : ∀ (ξ : Ξ) (x : X) (y : Y), ∑ i : O, ∑ j : O, q ξ x y i j = 1) (hA : ∀ (ξ : Ξ) (x : X) (y y' : Y) (i : O), marginalA (q ξ) x y i = marginalA (q ξ) x y' i) (hB : ∀ (ξ : Ξ) (x x' : X) (y : Y) (j : O), marginalB (q ξ) x y j = marginalB (q ξ) x' y j) (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (hmix : ∀ (x : X) (y : Y) (i j : O), ∫ (ξ : Ξ), q ξ x y i j ∂μ = Q x y i j) (A : ℕ → X) (B : ℕ → Y) (i : O) (n : ℕ) : ∫ (ξ : Ξ), |marginalA (q ξ) (A 0) (B 0) i - 1 / 2| ∂μ ≤ (chainCost Q o oc A B n + agree Q o oc (A 0) (B n)) / 2

★★★ Every component of a mixture inherits the chained bound. If each q ξ is a no-signalling two-outcome law and the mixture over ξ reproduces Q, then in mean over ξ the components' marginals at A 0 sit within 1 / 2 up to the bound computed from Q alone. So a chain on which Q is nearly perfectly correlated pins down not just Q's own marginal but every component's.

theorem ProbabilityTheory.ChainedBell.exists_signalling_of_sharp_integral {X : Type u_1} {Y : Type u_2} {O : Type u_3} [Fintype O] [DecidableEq O] {Ξ : Type u_4} [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ξ} {q : Ξ → X → Y → O → O → ℝ} {Q : X → Y → O → O → ℝ} {o oc : O} [MeasureTheory.IsProbabilityMeasure μ] (huniv : Finset.univ = {o, oc}) (hoc : oc ≠ o) (hnn : ∀ (ξ : Ξ) (x : X) (y : Y) (i j : O), 0 ≤ q ξ x y i j) (hsum : ∀ (ξ : Ξ) (x : X) (y : Y), ∑ i : O, ∑ j : O, q ξ x y i j = 1) (hint : ∀ (x : X) (y : Y) (i j : O), MeasureTheory.Integrable (fun (ξ : Ξ) => q ξ x y i j) μ) (hmix : ∀ (x : X) (y : Y) (i j : O), ∫ (ξ : Ξ), q ξ x y i j ∂μ = Q x y i j) (A : ℕ → X) (B : ℕ → Y) (i : O) (n : ℕ) (hsharp : (chainCost Q o oc A B n + agree Q o oc (A 0) (B n)) / 2 < ∫ (ξ : Ξ), |marginalA (q ξ) (A 0) (B 0) i - 1 / 2| ∂μ) : ¬((∀ (ξ : Ξ) (x : X) (y y' : Y) (i : O), marginalA (q ξ) x y i = marginalA (q ξ) x y' i) ∧ ∀ (ξ : Ξ) (x x' : X) (y : Y) (j : O), marginalB (q ξ) x y j = marginalB (q ξ) x' y j)

★ The contrapositive. A mixture whose components sharpen the marginal past the chained bound must contain a component that signals: no-signalling for every component is exactly what the bound needs.