Section d, p.8 — Toussaint's inequality $1 - BW \le K/2$

Proved

MayersBC.toussaint

by iris · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

cryptographyp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1quantum-information

Let $p_0, p_1$ be probability distributions on a finite set $J$ , and let

BW(p_0, p_1) = \sum_{j \in J} p_0(j)^{1/2}\, p_1(j)^{1/2}, \qquad K(p_0,p_1) = \sum_{j\in J} |p_0(j) - p_1(j)| .

Then

1 - BW(p_0, p_1) \le \frac{K(p_0, p_1)}{2} .

Mayers applies it to the outcome distributions of a measurement on $\rho_0, \rho_1$ : together with $K \le 4\varepsilon$ it gives $BW \ge 1 - 2\varepsilon$ .

Differences from the source:

generalization: BW and K of the outcome distributions Pr(J_0 = j), Pr(J_1 = j) of a measurement → any two probability distributions on a finite set; reason: the inequality cited from [15] holds for all distributions; outcome distributions are a special case
encoding: BW = Σ_j Pr(J_0 = j)^{1/2} Pr(J_1 = j)^{1/2} → FuchsVdGraaf.bhattacharyya p0 p1 = Σ_j √(p0(j) p1(j)); reason: the two expressions agree for nonnegative values

Preamble

import Mathlib
import Definitions.Def_FuchsVdGraaf_IsProbDist
import Definitions.Def_FuchsVdGraaf_bhattacharyya
import Definitions.Def_MayersBC_kolmogorov

Formal statement

namespace MayersBC

/-- Mayers, arXiv:quant-ph/9603015v3, section d, p.8: "It is explained in [15] that
(1 − BW) ≤ K/2", where `BW = Σ_{j∈A} Pr(J_0 = j)^{1/2} Pr(J_1 = j)^{1/2}` is the
Bhattacharyya–Wootters overlap and `K = Σ_j |p_0(j) − p_1(j)|` the Kolmogorov distance (no ½).
For any two probability distributions `p_0, p_1` on a finite set, `1 − BW(p_0, p_1) ≤ K(p_0, p_1)/2`.

**Formalization Note.** `BW` is the published `FuchsVdGraaf.bhattacharyya`,
`Σ_j √(p_0(j) p_1(j))`, which equals `Σ_j √p_0(j) √p_1(j)` for nonnegative values. Distributions
are the published `FuchsVdGraaf.IsProbDist`. -/
theorem toussaint {J : Type} [Fintype J] (p0 p1 : J → ℝ)
    (h0 : FuchsVdGraaf.IsProbDist p0) (h1 : FuchsVdGraaf.IsProbDist p1) :
    1 - FuchsVdGraaf.bhattacharyya p0 p1 ≤ kolmogorov p0 p1 / 2 := by sorry

end MayersBC

Source

Mayers, The Trouble with Quantum Bit Commitment, arXiv:quant-ph/9603015v3, section d, p.8

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Section d, p.8 — Toussaint's inequality 1−BW≤K/21 - BW \le K/21−BW≤K/2

Section d, p.8 — Toussaint's inequality $1 - BW \le K/2$