Appendix B, footnote 75: independent-link waiting distribution and mean

Proved

QAlgorithms.Papers.Independent.Gap48.P25.waitingDistribution

by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let two links have independent geometric waiting times on positive rounds, each with success probability $0<x\le1$ . Write $M$ for their maximum. Its nonnegative normalized distribution and finite mean satisfy, for $n\ge1$ ,

\Pr(M=n)=x(1-x)^{n-1}[2-(2-x)(1-x)^{n-1}],\qquad \mathbb E[M]={3-2x\over x(2-x)}.

The maximum distribution is constructed directly from the product of the geometric laws, and the expectation is a genuinely summable series. Also $x\mathbb E[M]\to3/2$ as $x\downarrow0$ . At $x=1$ the mean is one round. The excluded endpoint $x=0$ has infinite waiting time and is not assigned a real mean by this formula.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P25

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Gap48.P25

open scoped BigOperators ComplexConjugate

open Filter

open QAlgorithms.Papers.Independent.Claimed50.P08 (classicalEntropy)

/-- Footnote 75, PDF p.46: exact law and mean of two independent geometric
links. Includes x=1, excludes x=0 from the real expectation formula. -/
theorem waitingDistribution (x : ℝ) (hx : 0 < x ∧ x ≤ 1) :
    (∀ n, 0 ≤ twoLinkWaiting x n) ∧ HasSum (twoLinkWaiting x) 1 ∧
    (∀ n : ℕ, 1 ≤ n → twoLinkWaiting x n = x*(1-x)^(n-1)*(2-(2-x)*(1-x)^(n-1))) ∧
    HasSum (fun n : ℕ => (n : ℝ)*twoLinkWaiting x n) (waitingMean x) ∧
    Tendsto (fun z : ℝ => z*waitingMean z) (nhdsWithin 0 (Set.Ioi 0)) (nhds (3/2)) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 46, Appendix B, footnote 75: independent-link waiting distribution and mean

Read-back

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

For every real $x$ with $0<x\le1$ , define $g_x(0)=0$ and $g_x(n)=x(1-x)^{n-1}$ for natural $n\ge1$ , and define

w_x(n)=\sum_{i=0}^{n}\sum_{j=0}^{n} \begin{cases}g_x(i)g_x(j)&\max\{i,j\}=n,\\0&\text{otherwise},\end{cases} \qquad m(x)=\frac{3-2x}{x(2-x)}.

Then every $w_x(n)$ is nonnegative, $\sum_{n=0}^{\infty}w_x(n)=1$ , and for every natural $n\ge1$ ,

w_x(n)=x(1-x)^{n-1}\bigl(2-(2-x)(1-x)^{n-1}\bigr).

Also $\sum_{n=0}^{\infty}n\,w_x(n)=m(x)$ , and $\lim_{z\to0^+}z(3-2z)/(z(2-z))=3/2$ . The definition gives $w_x(0)=0$ ; $x=1$ is included, with zeroth powers interpreted as $1$ .

Human review

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

View graph