Probability

Motivation

The eigenvalues of a large non-Hermitian random matrix are hard to study directly. For Hermitian matrices, the empirical spectral distribution (ESD) is controlled by the resolvent and the Stieltjes transform, both stable under small perturbations. For non-Hermitian matrices no such tool exists: eigenvalues can move a long way under tiny perturbations, and the moment method fails because moments do not determine a measure on $\mathbb C$. The route that works, going back to Girko (1984) and used by Bai (1997), Götze–Tikhomirov (2007), Pan–Zhou (2007) and Tao–Vu (2008), passes through logarithmic determinants. The identity $\frac1n\log|\det(A-zI)|=\int\log|w-z|\,d\mu_A(w)$ links the ESD $\mu_A$ to a scalar quantity. That scalar is computable from the singular values of $A-zI$, which are eigenvalues of a Hermitian matrix.

Tao and Vu, with an appendix by Krishnapur (Ann. Probab. 38 (2010) 2023–2065), turn this link into an exact criterion. Theorem 1.15 of that paper states that the ESD of a normalized i.i.d. random matrix converges to a measure $\mu$ if and only if the normalized log-determinants converge to the logarithmic potential of $\mu$ for almost every $z$. The same holds for a regularized version built from the singular values. This mission formalizes Theorem 1.15 and the main steps of its proof (§8 and Appendix A of the published article).

Setting

Let $x$ be a complex random variable with $\mathbf E x=0$ and $\mathbf E|x|^2=1$, and let $(x_{ij})_{i,j\ge1}$ be independent copies of $x$ on a probability space $(\Omega,\mathbf P)$. For each $n$, $X_n=(x_{ij})_{1\le i,j\le n}$. Let $M_n$ be deterministic $n\times n$ complex matrices with

$$\text{(1.3)}\qquad\sup_n\frac1{n^2}\|M_n\|_2^2<\infty,\qquad\|M\|_2^2=\sum_{i,j}|m_{ij}|^2,$$

and put $A_n=M_n+X_n$.

For $A\in M_n(\mathbb C)$ with eigenvalues $\lambda_1,\dots,\lambda_n$, counted with algebraic multiplicity, the ESD is $\mu_A=\frac1n\sum_i\delta_{\lambda_i}$. Its singular values are $\sigma_1(A)\ge\dots\ge\sigma_n(A)\ge0$. A sequence of random measures $\mu_n$ converges in probability to a deterministic $\mu$ if, for every continuous compactly supported $f:\mathbb C\to\mathbb R$, $\int f\,d\mu_n-\int f\,d\mu$ tends to $0$ in probability. It converges almost surely if, with probability one, $\int f\,d\mu_n\to\int f\,d\mu$ for all such $f$ at once. The logarithmic potential of a measure $\mu$ is $z\mapsto\int\log|w-z|\,d\mu(w)$.

Hypothesis (1.4) states that, for almost every $z$, the ESDs of the deterministic matrices $(\frac1{\sqrt n}M_n-zI)(\frac1{\sqrt n}M_n-zI)^*$ converge to a limit.

In Lean everything lives in the namespace UnivESD.LogDet. The ESD is esd, the one-based singular value is sv, logPotential is the logarithmic potential, and ConvInProb/ConvAS/ESDConvInProb/ESDConvAS are the modes of convergence. IIDArray is the entry model, HSBound is (1.3), shiftA M xs z n ω is $\frac1{\sqrt n}A_n-zI$, and Cond14 is (1.4).

Formalization targets

Goal: Theorem 1.15

Let $\mu$ be a probability measure on $\mathbb C$ with $\int|z|^2\,d\mu<\infty$. The following are equivalent:

1. $\mu_{\frac1{\sqrt n}A_n}\to\mu$ in probability;
2. for a.e. $z$, $\displaystyle\frac1n\log\Big|\det\big(\tfrac1{\sqrt n}A_n-zI\big)\Big|\to\int_{\mathbb C}\log|w-z|\,d\mu(w)$ in probability;
3. for a.e. $z$ there are $\varepsilon_n>0$, $\varepsilon_n\to0$, with

$$\frac1n\log\det\Big(\big(\tfrac1{\sqrt n}A_n-zI\big)\big(\tfrac1{\sqrt n}A_n-zI\big)^*+\varepsilon_nI\Big)\to2\int_{\mathbb C}\log|w-z|\,d\mu(w)$$

in probability.

Under (1.4) the same equivalence holds with almost sure convergence throughout.

Milestones, in the order the proof uses them

• (8.1): for a.e. $z$, $w\mapsto\log|w-z|$ is $\mu$-integrable.
• Lemma A.3 (Weyl's comparison for products): $\prod_{j\le J}|\lambda_j|\le\prod_{j\le J}\sigma_j(A)$ and $\prod_{j\ge J}\sigma_j(A)\le\prod_{j\ge J}|\lambda_j|$.
• (8.3): $\mathbf P(\sigma_{n-i}\le ci/n)=O(\exp(-n^{0.01}))$ for $2n^{0.99}\le i\le n-1$.
• (8.2): $\frac1n\sum_{i=1}^n\big(\log\sqrt{\sigma_i^2+\varepsilon_n}-\log\sigma_i\big)\to0$ almost surely.
• p. 2057: almost surely, eventually, $\frac1n\sum_{(1-\kappa)n<i\le n}\log\frac1{\sigma_i}\le O(\kappa\log\frac1\kappa)$, and the same bound for $\log\frac1{|\lambda_i|}$.

Significance

Theorem 1.15 reduces convergence of a non-Hermitian ESD to a family of scalar limit statements. Each of these can be attacked through Hermitian tools, because the regularized log-determinant in (iii) is a smooth functional of the singular values. Corollary 1.16 of the paper derives from it a practical criterion: the ESD converges to $\mu$ once the singular value distributions of $\frac1{\sqrt n}A_n-zI$ converge for a.e. $z$ to laws $\eta_z$ with $\int\log t\,d\eta_z=2\int\log|w-z|\,d\mu$. With the universality principle (Theorem 1.5, the companion mission) and Mehta's computation for complex Gaussian matrices, this yields the circular law for i.i.d. matrices with finite variance.

The theorem is proved in the source. To our knowledge neither it nor any of its milestones has a machine-checked proof. Mathlib has the ingredients for the objects (characteristic polynomials and their roots, LinearMap.singularValues, the strong law of large numbers) but not the results. A formal proof would give the platform its first verified bridge between eigenvalue and singular value asymptotics. Lemma A.3 alone, Weyl's multiplicative majorization, is a standard linear-algebra fact absent from Mathlib.

Difficulty

Two things make the obvious argument fail. First, $\log$ is unbounded at $0$. Vague convergence of $\mu_{\frac1{\sqrt n}A_n}$ controls $\int f\,d\mu_n$ only for continuous compactly supported $f$, while $\log|w-z|$ has a singularity at $w=z$ and grows at infinity. Passing between (i) and (ii) therefore requires uniform control of the eigenvalues (and singular values) near $0$ after the shift: the contribution of the smallest ones must vanish. Second, eigenvalues are not stable under perturbation, so this control cannot be read off the eigenvalues. It has to come from the singular values, through a lower-tail bound on $\sigma_{n-i}$ that is exponentially small in a power of $n$, and through a deterministic inequality transferring bounds from singular values to eigenvalues. The smallest singular values ($i$ below $n^{0.99}$) need a separate polynomial lower bound (the paper's Lemma 4.1, posed in the companion mission). The tail bound in its printed form is false at that end of the range.

Formalization scope

Conventions committed to in Lean:

• The ESD is $n^{-1}$ times the sum of Dirac masses over the root multiset of the characteristic polynomial, so multiplicities are kept. Test functions are real-valued, continuous and compactly supported. Almost sure ESD convergence uses one null set for all test functions.
• The matrices $X_n$ are the top-left corners of one infinite i.i.d. array. In-probability statements do not depend on how the $X_n$ are coupled across $n$, but almost-sure statements do, and the paper's proof applies the strong law to this array. The limit in (1.4) is required to be a probability measure, which is equivalent under (1.3).
• The second-moment condition on $\mu$ is Integrable (‖w‖²) μ. The logarithmic potential is a Bochner integral, which is $0$ when not integrable; by (8.1) this happens only for a null set of $z$, which "for a.e. $z$" ignores.
• Real.log 0 = 0. In (ii), a singular matrix would contribute $0$ instead of $-\infty$; for this model the determinant is almost surely nonzero eventually. Every milestone with $\log\sigma_i$ or $\log|\lambda_i|$ carries positivity of those quantities in its conclusion.
• Singular values are one-based (sv A i is Mathlib's singularValues (i-1)). Eigenvalue enumerations are Fin n-indexed, and the paper's $\lambda_i$ is index $i-1$.
• The paper's $O(\cdot)$ constants are existential and fixed before $n$. In the $\kappa\log(1/\kappa)$ bounds the constant is fixed before $\kappa$; a $\kappa$-dependent constant would make the bounds empty.

Disclosed corrections to the printed text:

1. (iii)'s matrix. Theorem 1.15 prints a mis-bracketed product, and (1.8) prints $(C+\varepsilon_nI)(C^*+\varepsilon_nI)$. The Lean uses $CC^*+\varepsilon_nI$ with $C=\frac1{\sqrt n}A_n-zI$, the matrix of (8.2) and of the proof of Corollary 1.16.
2. (8.3)'s range. It is printed for $1\le i\le n-n^{0.99}$, which is false for small $i$: for Gaussian entries and $M_n=0$, $n\sigma_{n-1}$ has a non-degenerate limit law. It is posed on $2n^{0.99}\le i\le n-1$, the range the proof covers and the use needs.
3. Lemma A.3, second inequality. It is posed for $1\le J\le n$, since $\sigma_0$ is undefined. The eigenvalues are ordered $|\lambda_1|\ge\dots\ge|\lambda_n|$, not $|\lambda_1|\le\dots\le|\lambda_n|$ as printed: the printed order is a slip. With it, both inequalities are weaker than Weyl's and cannot support the use on p. 2057, which orders the eigenvalues decreasingly. The decreasing order implies the printed form.
4. (8.2) and (8.1). (8.2) is stated for every deterministic $\varepsilon_n>0$ with $\varepsilon_n\to0$; the proof uses nothing else. (8.1) is stated as $\mu$-integrability plus local integrability of $z\mapsto\int|\log|w-z||\,d\mu(w)$.

A trivializing formalization is ruled out by construction. The goal mentions only $A_n$ and $\mu$. The proof's comparison ensemble $B_n=\sqrt n\,\mathrm{diag}(\lambda_i)$ is not a hypothesis. No statement takes a log-potential or a log-determinant as an input that could be fixed to make it hold.

The companion mission (Theorem 1.5, universality) poses Theorem 2.1 (the replacement principle), Lemma 1.7 (tightness) and Lemma 4.1 (least singular value), which the proof here also uses. They are not restated here. Once that mission is published they belong here as references. Contributions are welcome on the linear-algebra layer (Lemma A.3, multiplicative Weyl majorization), the Fubini argument of (8.1), and the singular-value tail bound (8.3). These are reusable well beyond this paper.

Selected references

• T. Tao, V. Vu (appendix by M. Krishnapur), Random matrices: Universality of ESDs and the circular law, Ann. Probab. 38(5) (2010) 2023–2065. https://doi.org/10.1214/10-AOP534 (source of this mission; published version).
• V. L. Girko, The circular law, Teor. Veroyatnost. i Primenen. 29 (1984) 669–679. https://doi.org/10.1137/1129095
• Z. D. Bai, Circular law, Ann. Probab. 25(1) (1997) 494–529. https://doi.org/10.1214/aop/1024404298
• F. Götze, A. Tikhomirov, The circular law for random matrices, Ann. Probab. 38(4) (2010) 1444–1491. https://doi.org/10.1214/09-AOP522
• T. Tao, V. Vu, Random matrices: the circular law, Commun. Contemp. Math. 10(2) (2008) 261–307. https://doi.org/10.1142/S0219199708002788
• H. Weyl, Inequalities between the two kinds of eigenvalues of a linear transformation, Proc. Natl. Acad. Sci. USA 35 (1949) 408–411. https://doi.org/10.1073/pnas.35.7.408

Motivation

Supply disruptions — fires, quality failures, capacity shortfalls at a supplier — are a first-order risk in manufacturing supply chains. A buying firm has two broad responses. It can dual source, splitting orders between suppliers so that one supplier's shortfall is partly covered by the other, or it can invest in process improvement at a single supplier (kaizen events, supplier development programmes) to make that supplier more reliable. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), build a two-stage newsvendor model that captures both levers and compare them analytically.

This mission formalizes the paper's analysis of the improvement lever on its own: the firm commits early to one supplier, decides how much effort to spend improving it, and then orders. The paper's Theorem 3 shows that, without committed costs, this improvement problem is a concave program with an explicit first-order condition, and its Corollary 2 derives how the optimal effort responds to costs, revenue and the chance that improvement succeeds. These are the facts the paper's later comparisons between improvement and dual sourcing rest on.

Setting

A firm sells one product over one season at unit revenue $r$, salvage value $v$ and unit penalty $p$ for unmet demand. Demand $X \ge 0$ has distribution function $F$ and finite mean. The firm orders $q \ge 0$ units from a supplier with design capacity $K > 0$, unit cost $c$ and committed cost $\eta \in [0,1]$: the firm pays $(\eta q + (1-\eta)y)c$ when $y$ units are delivered.

The supplier suffers a random capacity loss $\xi \ge 0$ and delivers $y = \min\{q, (K-\xi)^+\}$. The law of $\xi$ has a continuous distribution function $G(\cdot, a)$ that depends on the supplier's reliability index $a$; a larger index means a stochastically smaller loss, $G(\cdot, a) \le G(\cdot, a')$ for $a \le a'$. Demand and losses are independent.

With $\psi = -\eta c/(r+p-v)$ and $\varphi = (r+p-(1-\eta)c)/(r+p-v)$, the second-stage expected profit at index $a$ is

$$\Pi_2(q; a) = (r+p-v)\big(\psi q + \varphi\,\mathsf E[y] - \mathsf E[(y-X)^+]\big) - p\,\mathsf E[X],$$

and $\Pi_2^*(a) = \sup_{q \ge 0}\Pi_2(q; a)$ is its optimal value.

In the first stage the firm may improve the supplier from its initial index $a^0$. The paper reparametrizes effort by the target index: reaching index $a \ge a^0$ needs effort $z(a)$, where $z$ is convex and nondecreasing with $z(a^0) = 0$. Effort costs $m$ per unit and succeeds with probability $\theta$. The first-stage profit of early commitment is Eq. (7):

$$\Pi_1(a) = -m\,z(a) + \theta\,\Pi_2^*(a) + (1-\theta)\,\Pi_2^*(a^0), \qquad a \ge a^0 .$$

Formalization targets

Goal: Theorem 3

Assume $\eta = 0$ and that $a \mapsto G(\xi, a)$ is concave on $[a^0,\infty)$ for every $\xi$ (decreasing marginal reliability improvement). Then $\Pi_1$ is concave on $[a^0, \infty)$, and an optimal index $a^* > a^0$, with an optimal order $q^*$ at $a^*$, satisfies

$$\frac{m}{\theta}\,z'(a^*) = (r+p-v)\int_{K-q^*}^{K}\big(\varphi - F(K-\xi)\big)\,\frac{\partial G(\xi, a^*)}{\partial a}\,d\xi. \tag{8}$$

Milestones

1. Eq. (6), single-supplier instance with $\eta = 0$. For $0 < \varphi < 1$ the critical fractile $\hat q = \inf\{t : F(t) \ge \varphi\}$ maximizes $\Pi_2(\cdot\,; a)$ for every index $a$, and (with atomless demand) every positive optimal order satisfies the $\eta = 0$ instance of (6), $G(K-q^*,a)(\varphi - F(q^*)) = 0$.
2. Lemma 2(b), single-supplier instance. $\Pi_2^*(a)$ is increasing in $a$.
3. Corollary 2 (a), (b), (c), (e). The optimal reliability index, and so the optimal effort $z^* = z(a^*)$, is decreasing in $m$, increasing in $\theta$, decreasing in $c$ and increasing in $r$, each in the strong set order on the set of maximizers.

Significance

Theorem 3 turns the firm's improvement decision into a one-dimensional concave program, so that the first-order condition (8) characterizes the optimum and comparative statics are available. Corollary 2 is the managerial content: cheaper or more reliable improvement, a cheaper supplier and a more valuable product all justify more improvement effort. The paper's later results — when late commitment beats early commitment (§4.2.2) and when single sourcing with improvement beats dual sourcing (§5) — compare the optimal values these results describe.

The results are proved in the paper's online appendix; none of them has a machine-checked proof. A complete development provides formal proofs of the layer-cake representation of the random-capacity newsvendor profit, of its critical-fractile solution, and of the concavity and envelope arguments on top of it.

Difficulty

$\Pi_2^*$ is an optimal value, a supremum over order quantities, and suprema of concave functions are not concave in general. The obvious route — "$\Pi_2(q; a)$ is concave in $a$ for each $q$, hence so is the supremum" — fails, because $\Pi_2(q;a)$ is not concave in $a$ for a fixed $q$ beyond the critical fractile. Any argument has to control how the optimal order moves with $a$ under random capacity, where the delivered quantity is a minimum of the order and a random effective capacity. The first-order condition then requires differentiating an expectation of a non-smooth function of $(\xi, X)$ in the parameter of $\xi$'s law. Corollary 2 must be argued on the set of maximizers, since $\Pi_1$ is concave but not strictly concave.

Formalization scope

The Lean development lives in the namespace MitigateSupplyRisk.Improvement. Model bundles $r, v, p, c, \eta, K$, a demand law $\mu$ and the family $\nu(a)$ of loss laws; $F$ and $G(\cdot,a)$ are their cdf. Expectations are Bochner integrals over $\nu(a)$ and over the product $\nu(a)\otimes\mu$. Model.Assumptions collects the standing assumptions of §3: $0 \le \eta \le 1$, $K > 0$, $v < r+p$ (implicit in the paper's division by $r+p-v$), a nonnegative integrable demand, nonnegative atomless losses, and the stochastic order in $a$. Demand needs no density. Effort bundles $\theta, m, a^0, z$ with $\theta \in [0,1]$, $m \ge 0$ and $z$ convex, nondecreasing on $[a^0,\infty)$, $z(a^0) = 0$; taking $z$ as primitive assumes every index $a \ge a^0$ is reachable. $\Pi_2^*$ is a real supremum and $\Pi_1$ is built from it, never from the critical fractile. Every statement about $\Pi_2^*$ carries $\eta = 0$ or $c \ge 0$, which makes the supremum finite. "Optimal" always means a maximizer over the whole feasible set, and "increasing" is weak throughout, as on p. 492 of the paper.

The paper's proofs are in an online appendix that was not used here. Deviations from the page, each disclosed in the item's Formalization Note:

• Eq. (8) omits the factor $r+p-v$ on its right side; it is correct as printed only when $r+p-v = 1$, which holds in all of the paper's numerical examples. The goal states the corrected identity, multiplied by $\theta$.
• $\partial^2 G/\partial a^2 \le 0$ is read as concavity of $G(\xi,\cdot)$ on $[a^0,\infty)$.
• (8) is the first-order condition at an interior optimum $a^* > a^0$; differentiability of $z$ and of $G(\xi,\cdot)$ at $a^*$ is assumed explicitly.
• Corollary 2 is stated in the strong set order on the argmax, (c) and (e) in the setting $\eta = 0$ of Theorem 3, and (b) with $c \ge 0$. Corollary 2(d), on the committed cost $\eta$, is not stated, because Theorem 3's setting fixes $\eta = 0$.
• Lemma 2(b) and Eq. (6) are the single-supplier instances of the paper's dual-sourcing statements, which the paper applies to single sourcing on p. 496.

A trivializing formalization is ruled out: $\Pi_1$ is built from the supremum $\Pi_2^*$ (not from $\Pi_2$ at a fixed order), the supremum is finite under the stated hypotheses, and every expectation is of an integrable function, so no statement holds through a junk value.

Reusable beyond this mission: the random-capacity newsvendor objects (delivered quantity, expected profit, layer-cake representation) and a Topkis-type monotone comparative statics lemma on a chain. Contributions of either, and proofs of the milestones in any order, are welcome.

Selected references

• Y. Wang, W. Gilland, B. Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement?, Manufacturing & Service Operations Management 12(3):489–510, 2010. https://doi.org/10.1287/msom.1090.0279
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• R. B. Handfield, D. R. Krause, T. V. Scannell, R. M. Monczka, Avoid the Pitfalls in Supplier Development, Sloan Management Review 41(2):37–49, 2000.

Motivation

Firms that buy from unreliable suppliers face two broad remedies: spread orders across several suppliers (dual sourcing), or invest in making a supplier more reliable (process improvement). Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single newsvendor model in which suppliers deliver less than ordered because of random capacity losses. This mission covers the first half of that comparison: the pure dual-sourcing strategy, in which the firm improves nobody and only chooses how much to order from each of two suppliers.

A single-supplier random-capacity model was studied by Ciarallo, Akella and Morton (Management Science 40(3), 1994); in that model, as the paper notes, the firm never orders more than demand to hedge against capacity shortfall. Dada, Petruzzi and Schwarz (M&SOM 9(1), 2007) studied several unreliable suppliers but gave only necessary conditions for optimal orders. The paper states necessary and sufficient conditions for two suppliers (its Theorem 1) and, for deterministic demand, a closed-form optimal order in each of six demand regions (Theorem 2). Its proofs are in an online appendix.

Setting

A product sells at unit revenue $r$, is salvaged at $v$, and unmet demand costs $p$ per unit, with $v < r + p$. Two suppliers $i = 1, 2$ have unit cost $c_i \ge 0$, committed-cost fraction $\eta_i \in [0, 1]$ and design capacity $K_i > 0$. Supplier $i$ suffers a random capacity loss $\xi_i \ge 0$ whose continuous distribution function $G_i(t, a_i)$ depends on a reliability index $a_i$: a larger index makes the loss stochastically smaller, $G_i(\cdot, a) \le G_i(\cdot, \hat a)$ for $a \le \hat a$. The losses are independent of each other and of demand $X \ge 0$, which has distribution function $F$.

For an order vector $q = (q_1, q_2) \ge 0$, supplier $i$ delivers $y_i = \min\{q_i, (K_i - \xi_i)^+\}$ and is paid $(\eta_i q_i + (1 - \eta_i) y_i) c_i$. The realized profit is

$$\pi(q) = -\sum_i (\eta_i q_i + (1-\eta_i) y_i) c_i + r \min\Big\{x, \sum_i y_i\Big\} + v\Big(\sum_i y_i - x\Big)^+ - p\Big(x - \sum_i y_i\Big)^+,$$

and the second-stage expected profit is $\Pi_2(q; a) = \mathbb E_{\xi(a), X}[\pi(q)]$. With $\psi_i = -\eta_i c_i/(r+p-v)$ and $\phi_i = (r + p - (1-\eta_i)c_i)/(r+p-v)$ this is the paper's Eq. (3). The optimal value is $\Pi_2^*(a) = \sup_{q \ge 0} \Pi_2(q; a)$, and an optimal procurement vector is a $q \ge 0$ attaining it.

Formalization targets

Goal: Theorem 2 (corrected)

Let demand be deterministic, $X = x \ge 0$, let $\eta = 0$, let $0 < \phi_i < 1$, let each $G_i$ be strictly increasing on a support $[0, b_i]$ with $b_i \le K_i$, and let $\phi_1 G_1(K_1) \ge \phi_2 G_2(K_2)$. With $A_1 = G_1^{-1}(\phi_2)$, $A_2 = G_2^{-1}(\phi_1)$, $B = G_1^{-1}(\tfrac{\phi_2}{\phi_1}G_2(K_2))$ and $S = K_1 + K_2$, an optimal vector is

$$q^* = \begin{cases} (x, 0) & 0 \le x \le K_1 - B \quad (\Omega_1)\\ (x - q_2^*, q_2^*),\ \phi_1 G_1(K_1 - x + q_2^*) = \phi_2 G_2(K_2 - q_2^*) & x \le S - (A_1 + A_2) \quad (\Omega_2)\\ (x - K_2 + A_2,\ x - K_1 + A_1) & x \le S - \max(A_1, A_2) \quad (\Omega_3)\\ (x - K_2 + A_2, K_2) \text{ if } A_1 \ge A_2, \text{ else } (K_1, x - K_1 + A_1) & x \le S - \min(A_1, A_2) \quad (\Omega_4)\\ (K_1, K_2) & \text{otherwise} \quad (\Omega_5 \cup \Omega_6).\end{cases}$$

In $\Omega_3$–$\Omega_5$ the firm orders more in total than demand: the quantity hedge.

Milestones

1. Lemma 1: $\Pi_2(q; a)$ is submodular in $q$, $\Pi_2(q \vee q') + \Pi_2(q \wedge q') \le \Pi_2(q) + \Pi_2(q')$.
2. Theorem 1: with a demand density, some optimal $q^*$ has, for each $i$, $q_i^* \in \{0, K_i\}$ or $\nabla_{q_i}\Pi_2(q^*; a) = 0$.
3. Eq. (6): for $0 < q_i < K_i$, $\nabla_{q_i}\Pi_2 = (r+p-v)\big(\psi_i + G_i(K_i - q_i)(\phi_i - \mathbb E[F(q_i + y_j)])\big)$, which vanishes at an optimal $q$.
4. Lemma 2(b): $\Pi_2^*(a)$ is increasing in each $a_i$.
5. Corollary 1 (after the goal): as either index increases, the hedge region $\Omega_3 \cup \Omega_4 \cup \Omega_5$ and the hedge size $[q_1^* + q_2^* - x]^+$ shrink; $\Omega_1$ expands in $a_1$ and contracts in $a_2$.

Significance

Theorem 2 is the paper's explicit description of how a buyer splits orders between two unreliable suppliers: single sourcing when capacity is ample, dual sourcing at total order equal to demand, then deliberate over-ordering, and finally ordering full capacity. The quantity hedge is the paper's main qualitative finding for dual sourcing, since, as the paper notes, over-ordering of this kind does not occur with one random-capacity supplier. Corollary 1 says how this hedge responds to reliability, which is the comparison with process improvement that the rest of the paper builds on; Lemma 2(b) is the value of reliability used there.

None of these results has a machine-checked proof, and the paper's proofs are in an online appendix not used here. A formalization would also settle the printed statement, which contains a slip (below) that a formal proof must avoid.

Difficulty

$\Pi_2$ is submodular but not jointly concave in $q$, so the usual route (concavity plus first-order conditions) is not available, and the paper invokes unimodality instead. Under deterministic demand $\Pi_2$ is not differentiable on the line $q_1 + q_2 = x$, where the $\Omega_1$ and $\Omega_2$ optima sit, so Theorem 1 cannot simply be specialized to Theorem 2: optimality there needs one-sided arguments. In every region the claim is global optimality over all $q \ge 0$, including orders above the design capacities, and the feasible set is unbounded.

Formalization scope

Suppliers are indexed by Fin 2 (index 0 is supplier 1). The capacity losses are a family of probability measures $\nu_i(a)$ on $\mathbb R$ without atoms and with $\nu_i(a)((-\infty, 0)) = 0$, and $G_i(t, a)$ is their distribution function. $\Pi_2$ is the Bochner integral of $\pi$ against $\nu_1(a_1) \otimes \nu_2(a_2) \otimes \mu$ for a demand law $\mu$. Every theorem assumes $\mu$ is a probability measure on $[0, \infty)$ with finite mean. Deterministic demand is $\mu = \delta_x$. Theorem 1 and Eq. (6) add $\mu \ll$ Lebesgue (the paper's density). "Optimal" means a global maximizer over $q \ge 0$, and "increasing" is weak, as the paper declares. Added standing hypotheses: $K_i > 0$, $v < r + p$, and $r, p, c_i \ge 0$, which bound $\pi$ above so that $\Pi_2^*$ is a genuine supremum. $G_i^{-1}$ is the generalized inverse $\inf\{t \ge 0 : G_i(t) \ge u\}$.

Corrections to the printed Theorem 2, each disclosed in its item:

• the $\min$ and $\max$ in the bounds of $\Omega_3$, $\Omega_4$, $\Omega_5$ are swapped back (as printed, $\Omega_4$ is empty and the $\Omega_3$ formula can exceed $K_1$);
• $G_i(K_i) = 1$ is added, through the support hypothesis (without it the $\Omega_1$ claim is false);
• $0 < \phi_i < 1$ and strict increase of $G_i$ on its support are added.

Theorem 1's "$q_i^* = K$" is read as $K_i$. Lemma 2(a) is not formalized: optimal orders are not unique and no reading of "$q_i^*$ is increasing" was found that is both faithful and safely true.

Stating Theorem 2 as "$q^*$ satisfies the first-order conditions", or optimality only within a region's face, would trivialize it; the statement requires $\Pi_2(q; a) \le \Pi_2(q^*; a)$ for every $q \ge 0$. Proofs need integrals of piecewise-linear functions of independent variables, differentiation under the integral sign, and facts about generalized inverses of continuous distribution functions. Lemma 1 and the generalized-inverse facts are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

• Y. Wang, W. Gilland, B. Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement?, Manufacturing & Service Operations Management 12(3):489–510, 2010. https://doi.org/10.1287/msom.1090.0279
• F. W. Ciarallo, R. Akella, T. E. Morton, A Periodic Review, Production Planning Model with Uncertain Capacity and Uncertain Demand — Optimality of Extended Myopic Policies, Management Science 40(3):320–332, 1994. https://doi.org/10.1287/mnsc.40.3.320
• M. Dada, N. C. Petruzzi, L. B. Schwarz, A Newsvendor's Procurement Problem when Suppliers Are Unreliable, Manufacturing & Service Operations Management 9(1):9–32, 2007. https://doi.org/10.1287/msom.1060.0126

Motivation

In a linearly parameterized bandit a decision maker repeatedly chooses an arm $u$ from a set $\mathcal U_r \subset \mathbb R^r$ and observes a noisy reward whose mean is linear in an unknown vector $Z$. The model covers problems in which many arms share a few underlying features: products described by a handful of characteristics, prices, or routes whose costs depend on a few parameters. Because the arms are correlated through $Z$, a good policy can learn about every arm from the rewards of any arm, and its regret can be made to depend on the dimension $r$ instead of on the number of arms, which may be infinite.

Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) prove an $\Omega(r\sqrt T)$ lower bound on the regret when the arms form the unit sphere, give a matching phase-based policy for strongly convex arm sets, and propose the Uncertainty Ellipsoid (UE) policy for arbitrary compact arm sets. The UE policy is close to the algorithms of Auer (2002) and Dani, Hayes and Kakade (2008), with two differences: it does not need to know the horizon $T$, and it allows $Z$ and the noise to be unbounded. This mission formalizes its regret bound for general compact arm sets, Theorem 4.1 of the paper.

Setting

Fix $r \ge 2$ and a compact set of arms $\mathcal U_r \subset \mathbb R^r$, with the Euclidean norm $\|v\| = \sqrt{v'v}$. Playing arm $u$ in period $t$ yields

$$X^u_t = u'Z + W^u_t,$$

where the noises $W^u_t$ are independent of each other and of $Z$, identically distributed in $t$ for each arm, and have mean zero. A policy chooses the arm $U_{t+1}$ of period $t+1$ as a function of the history $(U_1, X_1, \dots, U_t, X_t)$. The regret given $Z = z$ and the Bayes risk are

$$\mathrm{Regret}(z, T, \psi) = \sum_{t=1}^T \mathbb E\Big[\max_{v \in \mathcal U_r} v'z - U_t'z \,\Big|\, Z = z\Big], \qquad \mathrm{Risk}(T, \psi) = \mathbb E\big[\mathrm{Regret}(Z, T, \psi)\big].$$

Assumption 1 (p. 13) fixes constants $\sigma_0, \bar u, \lambda_0 > 0$ such that, for every $r \ge 2$: (a) $\mathbb E[e^{xW^u_t}] \le e^{x^2\sigma_0^2/2}$ for every arm and every $x \in \mathbb R$; (b) every arm has $\|u\| \le \bar u$, and $\mathcal U_r$ contains linearly independent arms $b_1, \dots, b_r$ with $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$.

The UE policy keeps the ordinary least squares estimate $\widehat Z_t = C_t\sum_{s \le t}U_sX_s$, where $C_t = (\sum_{s \le t}U_sU_s')^{-1}$, and, with $\kappa_0 = 2\sqrt{1 + \log(1 + 36\bar u^2/\lambda_0)}$ and $\alpha = 4\sigma_0\kappa_0^2$, the uncertainty radius

$$R^u_t = \alpha\sqrt{\log t}\,\sqrt{\min\{r\log t, |\mathcal U_r|\}}\;\|u\|_{C_t}, \qquad \|u\|_{C} = \sqrt{u'Cu}.$$

It plays $b_1, \dots, b_r$ in the first $r$ periods and then, in each period $t+1$, an arm maximizing $v'\widehat Z_t + R^v_t$ over $\mathcal U_r$, with ties broken arbitrarily.

Formalization targets

Goal: Theorem 4.1

There are constants $a_4, a_5 > 0$ depending only on $\sigma_0, \bar u, \lambda_0$ such that for every $r \ge 2$, every compact arm set satisfying Assumption 1, every run of the UE policy, all $T \ge r+1$ and all $z \in \mathbb R^r$,

$$\mathrm{Regret}(z, T, \mathrm{UE}) \le a_4\,r\|z\| + a_5\,r\sqrt T\log^{3/2}T, \qquad \mathrm{Risk}(T, \mathrm{UE}) \le a_4\,r\,\mathbb E\|Z\| + a_5\,r\sqrt T\log^{3/2}T.$$

The constants are not fixed: any positive values that work suffice.

Milestones

The proof in Appendix B proceeds through large deviation inequalities for adaptive least squares (Theorem B.1 for finitely many arms; Lemmas B.3, B.4, B.5 leading to Theorem B.2 for infinitely many), the radius bound $\Pr\{u'(\widehat Z_t - z) > R^u_t \mid Z = z\} \le 1/t^2$ (Lemma B.6), the instantaneous regret bound (Lemma B.7), the regret decomposition

$$\mathrm{Regret}(z, T, \mathrm{UE}) \le 2\bar u(r+2)\|z\| + 2\alpha\sqrt r(\log T)\sqrt T\;\mathbb E\Big[\sqrt{\textstyle\sum_{t=r}^{T-1}\|U_{t+1}\|^2_{C_t}} \;\Big|\; Z = z\Big]$$

(Lemma B.8), and the deterministic Lemmas B.9–B.11, which bound $\sum_{t=r}^{T-1}\|U_{t+1}\|^2_{C_t}$ by the value $V^*(\bar u^2/\lambda_0, T-r)$ of an optimization problem and that value by $O(r\log T)$.

Significance

Theorem 4.1 shows that one policy achieves regret within a factor $\log^{3/2}T$ of the $\Omega(r\sqrt T)$ lower bound for every compact arm set, finite or infinite, with sub-Gaussian unbounded noise and without knowledge of $T$. The dependence on the problem is only through $r$ and the three constants of Assumption 1; the number of arms does not appear. The large deviation inequalities of Appendix B.1 are also the input of the paper's Theorem 4.2 for finitely many arms.

The result is proved on paper; no machine-checked proof of it is known. A formal development would produce reusable components that are currently absent from Mathlib: a Chernoff-type bound for least squares estimates built from adaptively chosen regressors, the self-normalized inequality of De la Peña, Klass and Lai in the form of Lemma B.3, the determinant recursion behind Lemma B.9, and the law of a bandit history driven by a policy and an arm-dependent noise kernel.

Difficulty

The arms $U_s$ depend on past noise, so $\widehat Z_t - z = C_tM_t$ with $M_t = \sum_s U_sW_s$ is not a sum of independent terms with fixed weights, and the classical Chernoff bound does not apply. For finitely many arms a union bound over the possible pull counts suffices (Theorem B.1), but its bound grows like $t^{5|\mathcal U_r|}$ and is useless for infinite arm sets. Theorem B.2 instead needs a self-normalized martingale inequality and a covering argument over directions to compare $M_tM_t'$ with $C_t^{-1}$ in the Loewner order. A second difficulty is that the sum $\sum_t\|U_{t+1}\|_{C_t}$ of the radii played is not bounded term by term: each term can be as large as $\bar u^2/\lambda_0$, and only the multiplicative recursion of Lemma B.9 shows that large terms are rare.

Formalization scope

$\mathbb R^r$ is EuclideanSpace ℝ (Fin r), so norms are Euclidean. The constants $\bar u, \lambda_0$ are written ubar, lam0. Policies are deterministic, history-dependent and measurable (measurability is implicit in the paper). The noise is a Markov kernel $\nu$ giving the law of $W^u_t$ for each arm; the history given $Z = z$ is built period by period with fresh independent noise, which is the law of the paper's history. Assumption 1(a) is a bound on a lower Lebesgue integral, so it also asserts finiteness; $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$ is $x'(\sum_k b_kb_k')x \ge \lambda_0\|x\|^2$. The standing assumptions of Sec. 1.1 (compact $\mathcal U_r$, $r \ge 2$, independent mean-zero noise identically distributed in $t$) are hypotheses. $\min\{r\log t, |\mathcal U_r|\}$ equals $r\log t$ for an infinite arm set. A UE run is any measurable policy that plays $b_1, \dots, b_r$ first and then a maximizer of $v'\widehat Z_t + R^v_t$ after every history that starts with $b_1, \dots, b_r$; on those histories $C_t$ is a genuine inverse.

Deviations from the page, all disclosed in the items: Lemma B.4 is printed for $t \ge 1$ but its proof needs $t \ge r$, and at $t = 1$ the printed claim fails; it is stated for $t \ge r$. Lemmas B.4 and B.5 are printed without "$\mid Z = z$" and are stated for each fixed $z$, the form in which the paper uses them. Lemmas B.9 and B.10 ("with probability one") are stated for every arm sequence that starts with $b_1, \dots, b_r$ and stays in the ball of radius $\bar u$, which is stronger. Theorem B.1 carries the hypothesis that $\mathcal U_r$ is finite.

The regret is $T\max_v v'z$ minus the expected total reward, whose integrand is bounded, so it is never a junk value; the risk bound asserts integrability of the regret in $z$ and assumes $\mathbb E\|Z\| < \infty$. The constants $a_4, a_5$ are chosen before $r$, the arm set and the instance, so a formalization in which they depend on $r$ or on $\mathcal U_r$ does not prove the goal.

Welcome contributions include proofs of any milestone, in particular the deterministic Lemmas B.9–B.11, and reusable lemmas on matrix determinants, self-normalized bounds and bandit history measures. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers.

Selected references

• P. Rusmevichientong and J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010; preprint arXiv:0812.3465v2. https://arxiv.org/abs/0812.3465
• V. H. de la Peña, M. J. Klass and T. L. Lai, Self-normalized processes: exponential inequalities, moment bounds and iterated logarithm laws, Annals of Probability 32(3A), 2004. https://doi.org/10.1214/009117904000000397
• P. Auer, Using confidence bounds for exploitation-exploration trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. Dani, T. P. Hayes and S. M. Kakade, Stochastic linear optimization under bandit feedback, COLT 2008. https://www.learningtheory.org/colt2008/papers/80-Dani.pdf
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8

Motivation

A retailer that carries several substitutable products, such as brands of the same item, loses part of a customer's demand when the preferred product is out of stock, but not all of it: some customers buy another product instead. How much of each product to stock then depends on the stocking levels of the others. When all products are managed by one company, the stocking problem is a joint optimization; when each product is managed by a separate firm, it is a game, and each firm ignores the effect of its stock-outs on its competitors.

A common view in the inventory literature is that competition drives inventories up for every product. Mahajan and van Ryzin and Lippman and McCardle demonstrated it in special cases (Lippman & McCardle, Operations Research 1997; Mahajan & van Ryzin, Columbia working paper 1999, published in Operations Research 2001). Netessine and Rudi (SSRN 303779, 2002, later published in Operations Research, 2003) study the general model with $n$ products, an arbitrary continuous joint demand distribution, and arbitrary substitution fractions. They show that the common view fails in general: some products may be stocked more under centralized management (Proposition 6(i)), but at least one product is always stocked no less under competition (Proposition 6(ii)). This mission formalizes Proposition 6(ii) and the centralized first-order analysis on which it rests.

Setting

There are $n \ge 1$ products, indexed $i = 1,\dots,n$, sold in a single period. Product $i$ is stocked at $Q_i \ge 0$ units at unit cost $c_i$, sold at unit price $r_i$, and salvaged at unit value $s_i$, with $r_i > c_i > s_i > 0$. Write $u_i = r_i - c_i$ (the underage cost) and $o_i = c_i - s_i$ (the overage cost).

The first-choice demand vector $D = (D_1,\dots,D_n)$ is random, with a known continuous joint law on the positive orthant. A fraction $a_{ij} \in [0,1]$ of the unmet demand for product $i$ switches to product $j$, with $a_{ii} = 0$ and $\sum_j a_{ij} < 1$; a customer whose second choice is also out of stock is lost. The effective demand for product $i$ is

$$D^s_i = D_i + \sum_{j \ne i} a_{ji}\,(D_j - Q_j)^+, \qquad x^+ = \max(0,x).$$

Under centralized management a single company maximizes the expected profit

$$\pi(Q) = \mathbb E \sum_i \Big[r_i \min(D^s_i, Q_i) - c_i Q_i + s_i (Q_i - D^s_i)^+\Big]$$

over all $Q \ge 0$; a maximizer is written $Q^c$. Under competition firm $i$ chooses $Q_i \ge 0$ to maximize

$$\pi_i(Q) = \mathbb E\big[u_i D^s_i - u_i (D^s_i - Q_i)^+ - o_i (Q_i - D^s_i)^+\big],$$

given the other firms' quantities; a Nash equilibrium $Q^d \ge 0$ is a vector at which no firm gains by changing its own quantity. In the Lean development these objects are Model, Ds, centralProfit, IsCentralOptimal, firmProfit, IsBestResponse and IsNash in the namespace DemandSubstitution.Comparison.

Formalization targets

Goal: Proposition 6(ii)

For every optimal centralized stocking vector $Q^c$ and every Nash equilibrium $Q^d$,

$$\exists\, i:\quad Q^c_i \le Q^d_i .$$

The statement quantifies over all optima and all equilibria; it asserts neither existence nor uniqueness of either.

Milestones

1. The underage/overage form (1): $\pi = \mathbb E\sum_i [u_i D^s_i - u_i (D^s_i - Q_i)^+ - o_i (Q_i - D^s_i)^+]$.
2. The derivative of one substitution term: for $j \ne i$, $\partial\,\mathbb E(D^s_j - Q_j)^+/\partial Q_i = -a_{ij}\Pr(D^s_j > Q_j, D_i > Q_i)$.
3. The partial derivative (8) of $\pi$ with respect to $Q_i$.
4. Proposition 1, the centralized optimality condition (7):

$$\Pr(D_i < Q^c_i) - \Pr(D_i < Q^c_i < D^s_i) + \sum_{j\ne i}\frac{u_j+o_j}{u_i+o_i}\,a_{ij}\Pr(D^s_j < Q^c_j, D_i > Q^c_i) = \frac{u_i}{u_i+o_i}.$$

5. The comparison $\Pr(D^{sc}_i < Q^c_i) \le \Pr(D^{sd}_i < Q^d_i)$, where $D^{sc}$ and $D^{sd}$ are the effective demands at $Q^c$ and $Q^d$.

Significance

Proposition 6(ii) bounds how far competition can depart from the centralized solution in the downward direction: it can never make every product understocked. Together with Proposition 6(i), it shows that neither "competition overstocks everything" nor its opposite holds in general, and it is the step from which the symmetric case, Proposition 6(iii) (every product is stocked at least as much under competition), follows. The centralized condition (7) and the derivative (8) are of independent use: they give the first-order conditions of the multi-product newsvendor with stock-out substitution for an arbitrary number of products and an arbitrary continuous demand law, obtained without Leibniz-rule integration over polyhedral regions.

The results are proved in the paper; none of them has a machine-checked proof. A formal proof requires differentiating an expectation of piecewise-linear functions of the demand under the integral sign, and handling the measure-zero boundaries where those functions have kinks. That machinery is reusable for other multi-product newsvendor models.

Difficulty

The centralized profit is not concave in general for three or more products (the paper's own example, pp. 3–5), so the optimum cannot be characterized as the unique solution of first-order conditions: the argument must work with an arbitrary maximizer and use only the necessary condition at an interior coordinate. The derivative (8) must be justified as a two-sided derivative of an integral whose integrand is not differentiable on hyperplanes in demand space; the paper's difference quotient argument leaves the boundary terms implicit. Finally, the obvious comparison of the two first-order conditions yields only an inequality between probabilities; turning it into an inequality between stocking levels requires the distribution function of $D^s_i$ to be strictly increasing, and an optimal $Q^c_i$ may be zero, where (7) does not hold.

Formalization scope

Products are Fin n (0-based). The model data and the standing assumptions $r_i > c_i > s_i > 0$, $a_{ij} \in [0,1]$, $a_{ii} = 0$, $\sum_j a_{ij} < 1$ are fields of a structure Model n. The demand law is a probability measure $\mu$ on $\mathbb R^n$ that is absolutely continuous with respect to Lebesgue measure, is concentrated on the open positive orthant, and has integrable coordinates (IsDemandLaw). Expectations are Bochner integrals and probabilities are μ.real of sets with the strict and weak inequalities exactly as printed. Derivatives are two-sided HasDerivAt in one coordinate, the others held fixed through Function.update.

Three hypotheses are pinned relative to the page and disclosed in the statements:

• NeZero n in the goal: for $n = 0$ "at least one $i$" is false.
• HasPositiveDensity μ in the goal: a Lebesgue density strictly positive on the open positive orthant. The paper's last step uses strict monotonicity of the distribution function of $D^s_i$ without stating it.
• $Q^c_i > 0$ in Proposition 1 and in the probability comparison: (7) is an equality only at an interior coordinate. The goal carries no such hypothesis.

The centralized optimum is a maximizer of $\pi$ over nonnegative vectors and the Nash equilibrium is the no-profitable-deviation property over nonnegative quantities. Defining either by its first-order condition ((7) or (10)) would turn the propositions into definitions and is ruled out. Stating the goal for one chosen optimum or equilibrium is ruled out as well: it holds for every pair.

Contributions welcome: differentiation of expectations of piecewise-linear functions under absolutely continuous laws; null-set lemmas for $\{D^s_j = Q_j\}$; Fermat's rule at a coordinate-wise interior maximizer; the Nash condition (10) of the competitive game, which milestone 5 needs and which is also posed in the companion mission on equilibrium existence.

Selected references

• S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Simon School Working Paper OP 02-01, University of Rochester, April 2002, SSRN 303779. https://doi.org/10.2139/ssrn.303779 (journal version: Operations Research 51(2), 2003; this mission cites the working paper's numbering)
• S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 54–65, 1997.
• S. Mahajan and G. van Ryzin, Inventory competition under dynamic consumer choice, Columbia University working paper, 1999 (cited by Netessine & Rudi as [8]); published in Operations Research, 2001.

Motivation

Barabási and Albert (Science 1999) proposed preferential attachment as a mechanism behind the heavy-tailed degree distributions observed in the web graph and other networks: vertices arrive one at a time and attach to existing vertices with probability proportional to their degree. Empirical work on such networks reported that typical distances are very small compared with their size. The original description left the model underdetermined (the joint law of the $m$ edges of a new vertex was not specified), so its distances could not be analysed as stated.

Bollobás and Riordan (Combinatorica 2004) fixed a precise version of the model, the LCD model, and determined its diameter: for $m\ge2$ edges per vertex it is asymptotically $\log n/\log\log n$. For $m=1$ the graph is a forest (with loops), and a result of Pittel states essentially that its diameter is of order $\log n$. Together with the degree-sequence analysis of Bollobás, Riordan, Spencer and Tusnády (Random Struct. Alg. 2001), the paper is one of the first rigorous results on a scale-free random graph model.

Setting

The process $G_1^N$. Vertices are $1,\dots,N$. Vertex $t$ sends a single edge to a vertex $g_t\in\{1,\dots,t\}$, chosen given the past with

$$\mathbb P(g_t=i)=\frac{d_{G_1^{t-1}}(i)}{2t-1}\ (i<t),\qquad \mathbb P(g_t=t)=\frac1{2t-1},$$

where $d_{G_1^{t-1}}(i)$ is the degree of $i$ in the graph built so far (a loop counts twice). Loops ($g_t=t$) are allowed.

The graph $G_m^n$. Run $G_1^{mn}$ and identify the vertices $(k-1)m+1,\dots,km$ into a single vertex $k$, for $k=1,\dots,n$. The resulting random graph on $[n]$ is $G_m^n\in\mathcal G_m^n$. The paper's graph has loops and multiple edges; its diameter is the largest graph distance between two vertices of the underlying simple graph.

Almost every. For fixed $m$, a.e. $G_m^n$ has a property if its probability tends to $1$ as $n\to\infty$. All logarithms are natural.

The endpoint model (for the upper bound). Let $r_1,\dots,r_{mn}$ be independent with density $2x$ on $(0,1)$ ($M_2(0,1)$), $R_1\le\dots\le R_{mn}$ their sorted values, $W_i=R_{mi}$, $W_0=0$, $w_i=W_i-W_{i-1}$. Given $0<W_1<\dots<W_n<1$, the random graph $G(W_1,\dots,W_n)$ joins each vertex $i$ to $l_{i,1}$ and $l_{i,2}$, independent with $\mathbb P_L(l_{i,j}=k)=w_k/W_i$ for $k\le i$. The events $E_1,\dots,E_5$ (Lemma 7) say that the $W_i$ follow the profile $\sqrt{i/n}$ and that the spacings $w_i$ are neither too small nor too large in specified ranges.

Formalization targets

Goal: Theorem 1

For fixed $m\ge2$ and $\varepsilon>0$, a.e. $G_m^n$ is connected and

$$(1-\varepsilon)\frac{\log n}{\log\log n}\le\operatorname{diam}(G_m^n)\le(1+\varepsilon)\frac{\log n}{\log\log n}.$$

Lower bound (§4)

• Lemma 2: $\mathbb P(g_j=i)=O((ij)^{-1/2})$ and $\mathbb P(g_j=i,g_k=i)=O(i^{-1}(jk)^{-1/2})$ with absolute constants.
• Lemma 3: events $\bigcap\{g_{j_s}=i_s\}$ with disjoint sets of targets are negatively correlated.
• Lemma 4: $\mathbb P(S\subset G_1^N)\le C^{e(S)}\prod_{ij\in E(S)}1/\sqrt{ij}$ for graphs $S$ with at most one earlier and two later neighbours per vertex.
• Theorem 5: for every $m\ge1$, a.e. $G_m^n$ has $\operatorname{diam}(G_m^n)>\log n/\log(3Cm^2\log n)$, $C$ the constant of Lemma 4.

Upper bound (§§5–8)

• Lemma 6: Chernoff–Janson tails for sums of independent Bernoulli variables.
• Lemma 7: $\mathbb P(E_r)\to1$ for $r=1,\dots,5$.
• The coupling of §6: $G(W)$ with $W_i=R_{mi}$ is stochastically dominated by $G_m^n$ in the subgraph order, i.e. $\mathbb P(G(W)\in\mathcal P)\le\mathbb P(G_m^n\in\mathcal P)$ for every property $\mathcal P$ preserved under adding edges.
• Lemma 10 and Lemma 8: under $E_1,\dots,E_5$, every vertex reaches a useful vertex ($i\le n/(\log n)^5$, $w_i\ge(\log n)^2/n$) by a descending path of length at most $8\log\log n$, with probability $1-o(1)$.
• Lemma 12 (a deterministic growth estimate) and Lemma 11: a useful vertex is joined to vertex $1$ by a path of length at most $(1/2+\varepsilon)\log n/\log\log n$ with probability $1-o(n^{-1})$.
• The display of p. 29: under $E_1,\dots,E_5$, $\mathbb P_L\big(\operatorname{diam}G(W)>(1+\varepsilon/2)\log n/\log\log n+16\log\log n\big)=o(1)$.

Significance

The theorem shows that the diameter of this scale-free graph is smaller by a factor $\log\log n$ than that of a classical random graph with the same constant average degree, and identifies $m=1$ versus $m\ge2$ as the dividing line. It made the "small world" claims about the Barabási–Albert model precise for one exact version of it, and the LCD representation and the endpoint model introduced here were used in later work on preferential attachment.

The result is proved in the paper; nothing here is open. The work of the mission is formalizing the known proof. As far as is known, no machine-checked development of preferential-attachment graphs exists in Mathlib or elsewhere. A complete development would supply a reusable probability space for the attachment process, a Chernoff–Janson inequality for heterogeneous Bernoulli sums, a negative-correlation lemma for the process, and order-statistic estimates for i.i.d. samples, each of independent use.

Difficulty

The lower bound is a first-moment count of short paths, but the edges of $G_1^N$ are not independent: an earlier edge into a vertex raises the chance of later ones. Lemmas 2–4 show that small subgraphs still appear with probability comparable to an independent model with edge probabilities $C/\sqrt{ij}$; Lemma 3 requires a description of the process in which the needed independence is visible.

The upper bound is the hard half. A naive breadth-first expansion from a vertex fails: the weight of the next neighbourhood has the right mean but a very skewed distribution, and vertices near the end of the ordering have few early neighbours. The paper replaces the process by a conditionally independent model given the sorted endpoints $W_i$, controls the $W_i$ globally (Lemma 7), handles late vertices separately (Lemmas 8–10), and runs a weighted expansion with a growing blow-up factor (Lemmas 11–12). Each step needs uniformity in $W$: every $o(\cdot)$ must depend on $n$ only.

Formalization scope

Vertices are stored as Fin N (0-based) and statements read 1-based labels through the accessors tgt and lab. A sequence $(g_t)$ is a dependent function (t : Fin N) → Fin (t+1), its probability is the product of the exact conditional factors $(1+\#\{s<t: g_s=g_t\})/(2t-1)$, and probabilities are finite weighted sums. $G_1^N$, $G_m^n$ and $G(W)$ are Mathlib simple graphs: loops and multiple edges are dropped, which does not change connectivity or distances. The model is the paper's: not uniform attachment, not $m$ independent choices per vertex, and with the self-loop term.

$\operatorname{diam}$ in the goal is SimpleGraph.diam, which is $0$ on a disconnected graph; the goal therefore keeps connectivity explicit, as the page does. Every other diameter bound uses "every two vertices are joined by a walk of length $\le x$", and lower bounds use its negation, so a disconnected graph never satisfies an upper bound by default. Hidden constants follow the paper's quantifier order: the constants of Lemmas 2 and 4 come before every index; each $o(\cdot)$ of §§7–8 is a function $\delta(n)\to0$ chosen before $W$ (a bound chosen after $W$ would make these statements nearly empty); "for $n$ sufficiently large" is $\exists N_0$ before $W$ or $f$. Theorem 5 assumes the bound of Lemma 4 for its constant $C$. Every statement about $G(W)$ assumes $0=W_0<W_1<\dots<W_n<1$. Lemma 7 is stated as "the probability of the complement tends to $0$" under the product law of $M_2(0,1)$; the coupling is stated as the equivalent stochastic-domination inequality for every property preserved under adding edges.

Not formalized: Lemma 9 (a conditional bound given the history of a breadth-first exploration), the LCD representation of $G_1^n$ (§2), and Theorem 13 ($m=1$), which the paper states without proof.

Contributions welcome: proofs of any milestone, the identity $\mathbb P(g_j=i)=\mu_{j-1,i}/(2j-1)$ with $\mu_{t,i}=\prod_{s=i}^t(1+1/(2s-1))$, the LCD representation, and general lemmas about the attachment process and Bernoulli tails.

Selected references

• B. Bollobás and O. Riordan, The diameter of a scale-free random graph, Combinatorica 24(1):5–34, 2004. https://doi.org/10.1007/s00493-004-0002-2
• A.-L. Barabási and R. Albert, Emergence of scaling in random networks, Science 286:509–512, 1999. https://doi.org/10.1126/science.286.5439.509
• B. Bollobás, O. Riordan, J. Spencer and G. Tusnády, The degree sequence of a scale-free random graph process, Random Structures & Algorithms 18(3):279–290, 2001. https://doi.org/10.1002/rsa.1009
• S. Janson, T. Łuczak and A. Ruciński, Random Graphs, Wiley, 2000. https://doi.org/10.1002/9781118032718