Algorithmic Game Theory

Why mean field approximations on graphs need a threshold

Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate $O(1/\sqrt n)$ (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.

Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.

Setting

Let $G$ be a finite simple graph on the vertex set $V=\{1,\dots,n\}$; $u\sim v$ means $u$ and $v$ are adjacent and $\deg_G(v)$ is the number of neighbours of $v$. Fix a horizon $T>0$, a volatility $\sigma>0$ and a cost weight $c>0$. Each player $v\in V$ controls a real state $X_v$ through

$$dX_v(t)=\alpha_v(t,\boldsymbol X(t))\,dt+\sigma\,dW_v(t),\qquad t\in[0,T],$$

where $W_1,\dots,W_n$ are independent standard Brownian motions and $\boldsymbol X=(X_u)_{u\in V}$. A Markovian control $\alpha_v\in\mathcal A_G$ is a Borel function of time and the full state $\boldsymbol X(t)\in\mathbb R^V$, of linear growth. The cost of player $v$ under a profile $\boldsymbol\alpha=(\alpha_u)_{u\in V}$ is

$$J_v(\boldsymbol\alpha)=\frac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2\,dt+c\,\Big|X_v(T)-\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big],$$

and $\frac12\mathbb E[\int_0^T|\alpha_v|^2dt+c|X_v(T)|^2]$ for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector $\boldsymbol\varepsilon\in\mathbb R^V_+$, a profile is a Markovian $\boldsymbol\varepsilon$-Nash equilibrium if no player $v$ can lower its cost by more than $\varepsilon_v$ by switching unilaterally to another control $\beta\in\mathcal A_G$, written $(\beta,\boldsymbol\alpha^{-v})$.

The mean-field control is

$$\alpha^{\mathrm{MF}}(t,y)=\frac{-cy}{1+c(T-t)},\qquad \alpha^{\mathrm{MF}}_v(t,\boldsymbol x)=\alpha^{\mathrm{MF}}(t,x_v):$$

each player looks only at its own state, as if its neighbours' average were frozen at its mean.

Formalization targets

Goal: Theorem 2.11

Define $\epsilon^G_v=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{\deg_G(v)}}$ if $\deg_G(v)\ge1$ and $\epsilon^G_v=0$ if $\deg_G(v)=0$, and with the minimal degree $\delta(G)=\min_v\deg_G(v)$,

$$\epsilon_G=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{1\vee\delta(G)}}.$$

Then, with zero initial states, the state equation for $(\alpha^{\mathrm{MF}}_v)_{v\in V}$ has a solution, and

$$(\alpha^{\mathrm{MF}}_v)_{v\in V}\ \text{is an } \epsilon^G\text{-Nash equilibrium and an } \epsilon_G\text{-Nash equilibrium on } G.$$

Milestones

1. Lemma 7.2: $\alpha^{\mathrm{MF}}$ is optimal for the one-player problem $\min\frac12\mathbb E[\int_0^T\beta^2dt+c|Y(T)|^2]$, $dY=\beta\,dt+\sigma dW$, over all progressively measurable $\beta$.
2. Isolated vertices (p. 40): $J_v(\boldsymbol\alpha)=\inf_\beta J_v(\beta,\boldsymbol\alpha^{-v})$ when $\deg_G(v)=0$.
3. (7.7): under $\alpha^{\mathrm{MF}}$, $(X_u(T))_u$ are i.i.d. $N(0,\sigma^2T/(1+cT))$, so the neighbour average has second moment $\sigma^2T/(\deg_G(v)(1+cT))$.
4. Steps (1), (2), (3) (p. 41): a lower bound on $J_v(\beta,\boldsymbol\alpha^{-v})$, an energy bound for deviations no worse than the zero control, and the comparison with $J_v(\boldsymbol\alpha^{\mathrm{MF}})$.
5. (7.5): for $\deg_G(v)\ge1$ and every admissible $\beta$, $J_v(\beta,\boldsymbol\alpha^{-v})\ge J_v(\boldsymbol\alpha)-\epsilon^G_v$.

Significance

The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control $\alpha^{\mathrm{MF}}$ is an $\epsilon_{G_n}$-Nash equilibrium with $\epsilon_{G_n}\to0$, and the vector form says more: if the average of $(1\vee\deg_{G_n}(v))^{-1/2}$ over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate $\deg_G(v)^{-1/2}$ quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.

Difficulty

The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player $v$ couples its terminal state with the neighbours' average through a cross term $\mathbb E[\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\,Y_v(T)]$, and the deviation $\beta(t,\boldsymbol Y(t))$ may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.

Formalization scope

The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:

• vertices are Fin n (the paper's $\{1,\dots,n\}$ become $\{0,\dots,n-1\}$), the state space is EthierKurtz.SDEState n, and $G$ is any SimpleGraph (Fin n); isolated vertices are allowed;
• controls are Borel with linear growth on $[0,T]$ only; their values at other times are never used, and the formula for $\alpha^{\mathrm{MF}}$ outside $[0,T]$ is evaluated with Lean's total division;
• a solution of the state equation is a pathwise strong solution carrying its own probability space and an $n$-dimensional standard Brownian motion; costs are $[0,\infty]$-valued lower Lebesgue integrals, and the Nash inequality is required for every solution of the profile and of each deviation (faithful by strong uniqueness);
• $T,\sigma,c>0$ are the standing assumptions of §2.1;
• initial states are zero. The printed theorem does not mention $X(0)$; the paper fixes non-random initial states that are "in many cases" zero, and the whole proof is for $X(0)=0$. With non-zero initial states the claim fails in general, so this is a disclosed hypothesis;
• the goal also asserts that the state equation for $\alpha^{\mathrm{MF}}$ has a solution, so the Nash property cannot hold vacuously; Lemma 7.2 is stated over every continuous adapted solution of its SDE, and Step (2) carries, as an explicit hypothesis, the comparison with the zero control that its proof uses.

A formalization in which $\alpha^{\mathrm{MF}}$ is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.

Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47 (2022). https://arxiv.org/abs/2005.14102
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications II, Springer, 2018. https://doi.org/10.1007/978-3-319-56436-4
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6 (2006), 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• H. Pham, Continuous-time Stochastic Control and Optimization with Financial Applications, Springer, 2009 (verification theorem, Theorem 3.5.2). https://doi.org/10.1007/978-3-540-89500-8

Motivation

Mean field games describe Nash equilibria of large populations in which every player interacts with every other player symmetrically, through the empirical distribution of all states. Many systems of interest are not of this kind: agents in a network interact only with their neighbours, and the interaction structure is a graph rather than a complete graph. Understanding when equilibria on large graphs behave like mean field equilibria, and when they do not, requires models in which the equilibrium on a finite graph can be computed exactly.

Lacker and Soret (arXiv:2005.14102v2, Math. Oper. Res. 2022) introduced such a model: a linear–quadratic flocking game on an arbitrary finite graph, in which each player steers a Brownian particle and pays a terminal penalty for being far from the average of her neighbours. For vertex-transitive graphs they solved the game in closed form, up to a scalar ODE, with an equilibrium that depends on the graph only through the spectrum of its Laplacian. This mission formalizes that finite-graph result, Theorem 2.5 of the paper. Its large-graph consequences are the subject of missions II and III of this series.

Setting

Let $G$ be a finite simple graph on vertices $V=\{1,\dots,n\}$, with adjacency matrix $A_G$ and degree matrix $D_G$. When $G$ has no isolated vertices its random-walk Laplacian is

$$L_G := D_G^{-1}A_G - I .$$

$G$ is transitive if for every two vertices $u,v$ there is a graph automorphism mapping $u$ to $v$. A transitive graph is regular, so its Laplacian $L_G = A_G/\delta(G) - I$ is symmetric, with eigenvalues in $[-2,0]$.

Fix a horizon $T>0$, a noise level $\sigma>0$ and a cost constant $c>0$. Each vertex $v$ is a player with state

$$dX_v(t) = \alpha_v(t,X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],$$

driven by independent Brownian motions $W_v$, from a non-random initial state $X(0)=x_0\in\mathbb R^V$. A Markovian control $\alpha_v$ is a Borel function of time and the full state vector with at most linear growth. Player $v$ minimises

$$J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,X(t))|^2\,dt + c\,\Big|X_v(T)-\frac{1}{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].$$

A profile $(\alpha_v)_v$ is a Markovian Nash equilibrium if no player can lower her cost by switching unilaterally to another Markovian control.

The equilibrium is built from

$$Q_G(x) := \det(I-xL_G)^{1/n},\qquad f_G'(t) = c\,Q_G'(f_G(t)),\ f_G(0)=0,$$ $$P_G(t) := -f_G'(T-t)\,L_G\big(I-f_G(T-t)L_G\big)^{-1},\qquad \alpha^G_i(t,x) := -e_i^\top P_G(t)x .$$

Formalization targets

Goal: Theorem 2.5

For a finite transitive graph $G$ without isolated vertices:

1. $Q_G$ is well defined and continuously differentiable on $\mathbb R_+$, and the ODE has a unique solution $f_G:[0,T]\to\mathbb R_+$.
2. $(\alpha^G_i)_i$ is a Markovian Nash equilibrium for every initial state.
3. For every $t\in(0,T]$, the equilibrium state $X(t)$ is Gaussian with

$$\mathbb E X(t) = (I-f_G(T-t)L_G)(I-f_G(T)L_G)^{-1}x_0,\qquad \mathrm{Cov}\,X(t) = \sigma^2(I-f_G(T-t)L_G)^2\int_0^t(I-f_G(T-s)L_G)^{-2}\,ds .$$

4. The average equilibrium cost satisfies

$$\frac1n\sum_{v}J_v = \frac{|P_G(0)x_0|^2}{2\,\mathrm{Tr}\,P_G(0)} - \frac{\sigma^2}{2}\log\frac{\mathrm{Tr}\,P_G(0)}{n\,f_G'(T)} .$$

All four parts are in the goal statement.

Milestones

The milestones follow the paper's proof in §2.2, §3 and §4.

• Graph-spectral facts. Transitive graphs are regular with symmetric $L_G$ (§2.2). The spectrum of $L_G$ lies in $[-2,0]$ (Remark 2.4). The eigenvalue distribution $\mu_G$ has mean $-1$ ((3.2)), and $Q_G = Q_{\mu_G}$ (§2.3).
• The ODE. Bounds on $Q_\mu$ and its first two derivatives (Proposition 3.1), and well-posedness of $f_\mu' = cQ_\mu'(f_\mu)$ with explicit bounds (Proposition 3.2).
• Symmetry. Commutation of $L_G$ with automorphism matrices, and constancy of the diagonal of equivariant matrices (Lemma 4.1).
• The Riccati system. The properties of $P_G(t)$ (§4.4 (i)–(iii)), the reduction of the Nash PDE system to matrix Riccati equations (Lemma 4.2), and the verification that the explicit $F^i = (\mathrm{Tr}\,P/n)^{-1}Pe_ie_i^\top P$ solve them (§4.4).
• Law and value. The fundamental matrix $\exp(-\int_s^tP) = (I-f(T-t)L)(I-f(T-s)L)^{-1}$ (§4.5) and the averaged value identity (§4.6).

Significance

The result. Theorem 2.5 is one of the few explicit Nash equilibria of a stochastic differential game on a non-complete graph. Two features of it are not visible in mean field theory. The equilibrium controls are nonlocal: each player reacts to the whole state vector, not only to her neighbours. The whole equilibrium (law, value, controls) depends on the graph only through the spectrum of $L_G$. The second feature drives the paper's later results. Weak convergence of the eigenvalue distributions $\mu_{G_n}$ yields limits of the equilibrium, and these separate the dense regime, where the mean field approximation is valid, from the sparse regime, where it is not.

Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version of it or of its ingredients exists: the random-walk Laplacian of a graph, linear–quadratic stochastic differential games, verification theorems for Nash systems, and Gaussian laws of linear SDEs with time-dependent coefficients. The mission produces a checked statement of the equilibrium together with reusable layers: spectral facts about $D^{-1}A - I$, an ODE analysis for $Q_\mu$, and a Riccati reduction for quadratic Nash systems.

Difficulty

Three steps resist a direct approach.

• The verification theorem. The paper passes from a classical solution of the Nash system (4.1) to a Nash equilibrium by appeal to a standard verification argument. Over the full class of Borel controls with linear growth, this requires Itô's formula for the quadratic value functions, together with integrability of the deviated state processes.
• The Riccati system. The $n$ coupled matrix equations (4.6) have no general closed-form solution. The explicit solution exists only because transitivity forces $e_i^\top P(t)e_i = \mathrm{Tr}(P(t))/n$ for every $i$. That identity has to be derived from the action of the automorphism group (Lemma 4.1), not from regularity alone.
• The law of the state. It requires solving a linear SDE with a time-dependent matrix and identifying its Gaussian law, a step for which the library has little support.

Formalization scope

Lean conventions:

• Vertices. The vertex set is Fin n, so the paper's $1,\dots,n$ become $0,\dots,n-1$. The state space is the platform's EthierKurtz.SDEState n (Euclidean $\mathbb R^n$).
• The Laplacian. $L_G$ is the random-walk Laplacian $D^{-1}A-I$, not Mathlib's $D-A$.
• Time and controls. Time is real. Controls are Borel on $\mathbb R\times\mathbb R^n$ with linear growth on $[0,T]$; their values off $[0,T]$ are never used.
• Solutions of (2.1). A solution is a pathwise strong solution on a probability space that the solution itself carries, adapted to the completed Brownian filtration. Costs are compared across solutions; this is faithful because (2.1) has a unique strong solution.
• Costs are $[0,\infty]$-valued lower Lebesgue integrals. They are converted to reals only after their finiteness is asserted.
• Existence of the equilibrium state. The goal also asserts that the equilibrium state equation has a solution, so that the Nash property cannot hold vacuously.
• Derivatives. $f_G'(T-t)$ is written as its ODE value $cQ_G'(f_G(T-t))$. The ODE is solved on $[0,T]$ with one-sided derivatives at the endpoints, and uniqueness is agreement on $[0,T]$.
• Matrix conventions. Covariance integrals are entrywise. Gaussian laws are Mathlib's multivariateGaussian.
• Added hypotheses. $0<n$ is added to three milestones that are false on the empty graph.

A formalization that fixes $x_0=0$, restricts deviations to linear controls, drops the existence of the equilibrium state process, or replaces $L_G$ by $D-A$ is not this theorem.

Infrastructure that a complete development needs:

• symmetric-matrix spectral calculus for $L_G$ and for the matrix functions $(I-xL)^{-1}$ and $\log(I-xL)$;
• differentiation under the integral for $Q_\mu$;
• Picard–Lindelöf and Grönwall on $\mathbb R_+$;
• Itô's formula for quadratic functions of a diffusion with additive noise;
• the Gaussian law of $\int_0^t M(t,s)\,dW_s$ for deterministic $M$.

The spectral, ODE and Riccati layers are reusable beyond this mission. Proofs of individual milestones are welcome; so are general verification theorems for linear–quadratic games.

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47(2), 2022. https://arxiv.org/abs/2005.14102
• F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• A. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39(3), 1981. https://doi.org/10.1070/SM1981v039n03ABEH001522

Motivation

A recurring question in revenue management with strategic consumers is whether a seller gains from price commitment. When customers are forward-looking, a seller who announces its whole price path in advance (pre-announced pricing) removes the customers' incentive to wait for a markdown the seller would otherwise be tempted to give; a seller who keeps the freedom to set later prices after observing the market (responsive pricing) cannot credibly promise not to cut prices. In the classical models without learning, commitment is valuable: Aviv and Pazgal (2008) find that announced pricing extracts more profit than contingent pricing from forward-looking customers, and Besanko and Winston (1990) analyse the responsive monopolist facing rational consumers.

Papanastasiou and Savva (Management Science, 2017) add social learning (SL): early buyers post product reviews, and the customers still in the market update their beliefs about the product's quality before deciding whether to buy later. The reviews create an informational reason to wait, and they also give the responsive seller something to respond to. This mission formalizes the paper's §7, which asks whether commitment remains valuable once learning is present, and its answer: for impatient consumers it is not.

Setting

A monopolist sells over two periods to a continuum of consumers of mass one. Consumer $i$ has a preference $x_i$, uniform on $[0,1]$. Mean product quality is unknown; consumers share the prior $\tilde q_p \sim N(0,\sigma_p^2)$, and reviews carry noise of variance $\sigma_q^2$. The SL parameter is $\gamma = \sigma_p^2/\sigma_q^2 \ge 0$. Consumers discount second-period utility by $\delta_c \in [0,1]$; the firm does not discount; the unit cost is $c \in [0,1)$.

If a mass $n_1$ of consumers buys in period 1, the posterior mean $q_u$ that the remaining consumers see is, before the reviews arrive, distributed as

$$q_u \sim N\Big(0,\ \sigma_p^2\,\frac{n_1\gamma}{n_1\gamma+1}\Big),$$

the pre-posterior law (Lemma 1); when $n_1\gamma = 0$ it is the point mass at $0$. A remaining consumer of type $x$ who buys in period 2 at price $p_2$ gets $x + q_u - p_2$.

• Pre-announced pricing. The firm commits to $\{p_1,p_2\}$. A measurable set $B\subseteq[0,1]$ of first-period buyers is a purchasing equilibrium if each $x\in B$ weakly prefers buying now, $x-p_1 \ge \max\big(0,\ \delta_c E[(x+q_u-p_2)^+]\big)$, and each other type weakly prefers to wait, where $q_u$ has the pre-posterior law for $n_1 = |B|$. The profit is $(p_1-c)|B| + (p_2-c)\,E\,|\{x\notin B : x+q_u\ge p_2\}|$.
• Responsive pricing. The firm sets $p_1$, observes $q_u$ and then sets $p_2 = s(q_u)$, where $s$ must maximize the second-period profit $(p_2-c)\,|\{x\notin B: x+q_u\ge p_2\}|$ at every $q_u$; $B$ is a purchasing equilibrium given $s$. Lemma 3 identifies the optimal second-period price $p_2^*(q_u,\bar x)$ of equation (6), where $\bar x$ is the remaining mass.

The optimal values $\pi^*_p$ and $\pi^*_r$ are the suprema of expected profit over all prices and all equilibria. In Lean these are preValue P and respValue P for a parameter record P : Params, and P.withδc d is the same model with discount factor $d$; "absence of SL" is P.noSL, the same model with $\gamma = 0$.

Formalization targets

Goal: Proposition 8

In the presence of SL there is a threshold $T(\gamma)\in(0,1]$ such that

$$\pi^*_p(\delta_c) < \pi^*_r(\delta_c)\qquad\text{for all }\delta_c\in[0,T(\gamma)],$$

with $\sigma_p$, $\gamma > 0$ and $c$ fixed on both sides. The threshold is not specified; only its positivity is claimed.

Milestones

1. For $\delta_c = 0$ the pre-announced purchasing threshold is $\theta(p_1,p_2) = p_1$ (proof of Example 1).
2. Lemma 3: the second-period price (6) is optimal for every $q_u$, $\bar x$, uniquely so outside the exit region.
3. For $\delta_c = 0$ the responsive purchasing threshold is $\zeta(p_1) = p_1$ (proof of Lemma 4).
4. With SL and $\delta_c = 0$: $\pi^*_p < \pi^*_r$.
5. With SL, $\pi^*_p$ and $\pi^*_r$ are finite and continuous in $\delta_c\in[0,1]$.

Companion: Proposition 7

Without SL ($\gamma = 0$), both values are finite and

$$\pi^*_{bp}-\pi^*_{br} = \frac{\delta_c^2(1-c)^2(1-\delta_c)}{4(9-2\delta_c^2-3\delta_c)} \ge 0,$$

strictly positive for $\delta_c\in(0,1)$.

Significance

The two propositions together reverse a standard prediction. Without learning, commitment weakly dominates (Proposition 7, consistent with Aviv and Pazgal 2008). With learning and impatient consumers, flexibility strictly dominates (Proposition 8): the value of reacting to reviews outweighs the cost of being unable to commit. The paper's numerical study (Figure 4) suggests that the threshold equals one for moderate $\gamma$, so that responsive pricing wins for every discount factor; that numerical claim is not a theorem of the paper and is not posed here.

The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. Formalizing them requires a rigorous treatment of a continuum purchasing game whose equilibrium is defined through a Gaussian law whose variance depends on the equilibrium itself, the subgame-perfect second-period pricing rule, and the continuity of optimal values in a parameter.

Difficulty

The comparison at $\delta_c = 0$ is elementary in spirit: myopic consumers buy early exactly when $x\ge p_1$, so the two regimes produce the same reviews for the same $p_1$, and the responsive firm can only do better state by state. Turning this into a strict inequality between two suprema requires a uniform gap, not just a pointwise one, because the paper's argument assumes an optimal pre-announced plan exists.

The step that extends the result to $\delta_c > 0$ is the paper's appeal to the Maximum Theorem. It needs the expected profit to be jointly continuous in the prices and in $\delta_c$ over a compact set of relevant plans. But the expected profit depends on $\delta_c$ through the equilibrium threshold, which is defined implicitly by an indifference equation whose Gaussian kernel itself depends on the threshold (equations (3) and (9)), and equilibria are sets of types, not numbers. Continuity of the optimal value therefore requires continuity and uniqueness of these implicit thresholds, and a reduction of both suprema to compact sets of prices.

Formalization scope

The model is one shared definition module (SLPricing.Compare.Model), plus the formula (6) as p2Star. Conventions it commits to:

• Standing assumptions $\sigma_p > 0$, $\gamma\ge0$, $\delta_c\in[0,1]$, $c\in[0,1)$; the firm's discount factor is $1$; pure strategies.
• Consumer types are $[0,1]$ with Lebesgue measure; equilibria use weak best responses, so buyer sets are unique only up to null sets.
• The benchmark "absence of SL" is $\gamma = 0$, where the pre-posterior law is the Dirac mass at $0$ (the paper's limit $\gamma\to0$).
• The responsive second-period rule $s$ is measurable and optimal at every realization of $q_u$; in the exit region $q_u\le c-\bar x$ any maximizer is allowed, since every one sells nothing.
• Optimal values are extended-real suprema over all real prices and all equilibria.

Added hypotheses, disclosed in each item: $p_1\in[0,1]$ in the two threshold milestones; $\bar x > 0$ for the uniqueness clause of Lemma 3. Proposition 7's "higher" is stated as the proof states it: non-negative gap on $[0,1]$, strict on $(0,1)$.

The comparison is meaningful only because the responsive firm cannot commit. Enlarging the responsive regime to arbitrary second-period rules, or defining either optimal value as a real supremum (whose junk value is $0$ on unbounded sets), would make the goal trivial or empty; both are excluded by the definitions. Hard-wiring the thresholds $\theta$, $\zeta$ or the price (6) into the definitions would make the milestones definitional; they are theorems here.

A complete development needs: Gaussian expectations of piecewise-linear functions of $q_u$ and their continuity in the variance; the implicit-function argument for the thresholds; a Maximum Theorem (Berge) for the optimal values. The Gaussian convex-order and Maximum-Theorem pieces are reusable well beyond this mission, and contributions of them as separate theorems are welcome.

Selected references

• Y. Papanastasiou, N. Savva, Dynamic Pricing in the Presence of Social Learning and Strategic Consumers, Management Science 63(4):919–939, 2017. https://doi.org/10.1287/mnsc.2015.2378 (accepted manuscript MS-14-00028.R2, 2016, is the source of all indices).
• Y. Aviv, A. Pazgal, Optimal pricing of seasonal products in the presence of forward-looking consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• D. Besanko, W. L. Winston, Optimal price skimming by a monopolist facing rational consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996 (Theorem 9.14, the Maximum Theorem). https://doi.org/10.1017/CBO9780511804526

Motivation

A firm launching a new experience good does not know how good the product is, and neither do its customers. Early buyers post reviews, and customers who wait learn from them: this is social learning (SL). Forward-looking customers anticipate this and may delay their purchase until reviews are available, which cuts into the firm's early sales. Papanastasiou and Savva (Management Science 2017) ask whether SL helps or hurts a monopolist facing such strategic consumers.

This mission formalizes their answer for responsive pricing, where the firm cannot commit to a second-period price and instead sets it after observing the reviews. Without learning, this is the classical price-skimming game of Besanko and Winston (1990), in which a firm without commitment power is hurt by consumer patience. With learning, two effects compete: reviews make the second-period market more informative (an informational effect the firm can exploit by repricing), and the option to learn makes waiting more attractive (a behavioral effect that hurts the firm).

Setting

A monopolist sells over two periods at unit cost $c\in[0,1)$ to a unit mass of consumers with preference types $x$ uniform on $[0,1]$. The mean quality is unknown, with prior $N(0,\sigma_p^2)$, and reviews are noisy with variance $\sigma_q^2$; the SL influence parameter is $\gamma=\sigma_p^2/\sigma_q^2\ge0$. Consumers discount second-period utility by $\delta_c\in[0,1]$; the firm does not discount.

If a set $B\subseteq[0,1]$ of types buys in period 1, its mass $|B|$ is the mass of reviews, and the posterior mean $q_u$, seen from period 1, has the pre-posterior law $N\big(0,\sigma_p^2\,\tfrac{|B|\gamma}{|B|\gamma+1}\big)$ (Lemma 1 and Definition 1 of the paper). In period 2 the remaining types value the product at $x+q_u$.

Under responsive pricing the firm sets $p_1$; consumers decide whether to buy now or wait; reviews realize $q_u$; the firm sets $p_2=s(q_u)$ to maximize the second-period profit

$$\pi_2(p_2)=(p_2-c)\,\big|\{x\in[0,1]\setminus B:\ x+q_u\ge p_2\}\big|.$$

An equilibrium after $p_1$ is a measurable buyer set $B$ and a measurable rule $s$ that is optimal at every $q_u$, such that every type in $B$ weakly prefers $x-p_1$ to the discounted expected value $\delta_c\,\mathbb E[(x+q_u-s(q_u))^+]$ of waiting, and every type outside $B$ weakly prefers waiting. The firm's expected profit is $\pi_r=(p_1-c)|B|+\mathbb E[\pi_2(s(q_u))]$, and $\pi_r^*$ is its supremum over all $p_1$ and all equilibria. The benchmark "absence of SL" ($\gamma\to0$ in the paper) is the same model at $\gamma=0$, where $q_u=0$ with certainty.

Formalization targets

Goal: Proposition 6

$$\gamma>0\ \Longrightarrow\ \exists\,\Delta_{lr}\in(0,1],\ \Delta_{hr}\in[0,1):\quad \delta_c\le\Delta_{lr}\ \text{or}\ \delta_c\ge\Delta_{hr}\ \Longrightarrow\ \pi_r^*\big|_{\gamma}>\pi_r^*\big|_{\gamma=0}.$$

The thresholds are left unspecified; the statement asserts only that SL raises the optimal profit near both ends of the patience range.

Milestones

1. Lemma 3: the second-period price $p_2^*(q_u,\bar x)$ of (6) is optimal when $[0,\bar x)$ remains.
2. (5): without SL, the first-period buyers are the types $x\ge\chi(p_1)=\frac{2p_1-c\delta_c}{2-\delta_c}$.
3. Proposition 4: the benchmark optimum $p_1^*=\frac{2c+\delta_c^2(1-c)+4(1-\delta_c)}{6-4\delta_c}$, $p_2^*=\frac{\chi(p_1^*)+c}{2}$, and monotonicity in $\delta_c$.
4. Lemma 4: with SL, the first-period threshold $\zeta(p_1)$ solves the implicit equation (7).
5. (8): the expected profit as a function of the threshold (with a corrected integrand).
6. Proposition 5: adoption inertia is never optimal; the on-path second-period price.
7. Example 3: the endpoint $\delta_c=0$.
8. Continuity of $\pi_r^*$ in $\delta_c\in[0,1]$ (proof of Proposition 6).

Significance

The result shows that the benefit of reviews to a firm that reprices dynamically, previously established for non-strategic consumers, survives when consumers strategically wait for information. It is one half of the paper's comparison between commitment and responsiveness: under SL the firm's flexibility to react to reviews becomes valuable, which reverses the classical ranking of pre-announced over responsive pricing.

The paper proves the result on paper only. This mission produces a machine-checked model of a two-period game with a continuum of consumers, Bayesian learning and subgame-perfect pricing, and machine-checked versions of the equilibrium characterizations. The paper's numerical evidence that the result holds for all $\delta_c$ is not part of the goal.

Difficulty

The first-period threshold is defined implicitly: in (7) the law of $q_u$ has a variance that depends on the threshold itself, and the second-period price inside the integral is a piecewise function of both. Existence, uniqueness and the comparison with the benchmark all go through this fixed-point equation.

The endpoint $\delta_c=1$ relies on Proposition 5(i), that inducing adoption inertia is strictly suboptimal. At $\delta_c=1$ the alternative price used in the printed proof yields exactly the inertia profit, so this endpoint is not settled by the page's witness. Passing from the two endpoints to the thresholds requires continuity of an optimal value taken over an unbounded price set and over implicitly defined equilibria; the paper cites the Maximum Theorem, whose hypotheses must be established.

Formalization scope

Everything lives in namespace SLPricing.Resp. The model file is shared, verbatim, with the two other missions of this series. Conventions:

• Standing assumptions: $\sigma_p>0$, $\gamma\ge0$, $\delta_c\in[0,1]$, $c\in[0,1)$; firm discount factor $1$; pure strategies.
• Best responses are weak, so buyer sets are unique only up to null sets.
• The second-period rule must be optimal at every realization and measurable. In the exit region $q_u\le c-\bar x$ every optimal price sells nothing; (6)'s value $c$ is a convention there.
• Optimal values are suprema in EReal over all real prices and all their equilibria, so neither an empty nor an unbounded family produces a junk value. Defining $\pi_r^*$ as the profit at a closed-form price, or the benchmark by dropping the second period, would make the goal circular; the formalization does neither.
• The thresholds are in the half-open intervals of the page; closed intervals would make the goal trivial.

Hypotheses added or restricted relative to the page, each disclosed in its item:

• (5) assumes $p_1\ge c$ (the printed formula is wrong below cost) and states uniqueness for $\delta_c<1$ (at $\delta_c=1$ non-threshold equilibria exist).
• Proposition 4 states uniqueness only for $\delta_c<1$ (at $\delta_c=1$ every $p_1\ge(1+c)/2$ is optimal).
• Lemma 4 assumes $p_1\ge0$; its monotonicity sentence is not posed.
• Lemma 3's uniqueness assumes $\bar x>0$ and $q_u>c-\bar x$.
• (8) is stated with last integrand $\zeta(q_u-c)$; the page prints $\zeta q_u$, which contradicts the proof of Lemma 3.

Contributions welcome: Gaussian integral estimates for (7), the second-period optimization of Lemma 3, a witness against inertia at $\delta_c=1$, and a continuity argument for optimal values over parametrized equilibria, which is reusable for the series' other missions.

Selected references

• Y. Papanastasiou, N. Savva, Dynamic Pricing in the Presence of Social Learning and Strategic Consumers, Management Science 63(4):919–939, 2017. https://doi.org/10.1287/mnsc.2015.2378 (cited from the accepted manuscript MS-14-00028.R2, 2016)
• D. Besanko, W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
• Y. Aviv, A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

Motivation

Online reviews let consumers learn about a new product from the experience of earlier buyers. For a firm selling to strategic consumers, who time their purchases, this social learning (SL) cuts two ways. Reviews reveal quality, which can raise second-period demand; but a consumer who expects reviews also has a new reason to wait, and every consumer who waits writes no review. Papanastasiou and Savva (Management Science 63(4), 2017) build a two-period model in which both forces are endogenous and ask whether a monopolist that commits to its prices in advance is better or worse off when consumers learn from one another.

The benchmark without learning is the classical intertemporal pricing problem with strategic consumers (Landsberger and Meilijson, 1985), whose optimal pre-announced plan is a decreasing price path. This mission formalizes the paper's answer for pre-announced pricing: its Proposition 3.

Setting

A unit mass of consumers has preference types $x$ uniform on $[0,1]$. A product of unknown mean quality $\hat q$ is sold over two periods. Buying in period $t$ gives type $x$ the utility $\delta_c^{t-1}(x+q-p_t)$, where $\delta_c\in[0,1]$ is the consumers' discount factor and $q$ the perceived quality. The firm has unit cost $c\in[0,1)$ and does not discount.

Everyone shares the prior $\hat q\sim N(0,\sigma_p^2)$. Individual quality perceptions are $N(\hat q,\sigma_q^2)$, and $\gamma=\sigma_p^2/\sigma_q^2$ is the SL influence parameter. If a mass $n_1$ buys in period 1 and posts reviews, the posterior mean is $q_u=\tfrac{n_1\gamma}{n_1\gamma+1}R$, where $R$ is the average rating. Seen from period 1, $q_u$ is random, with the pre-posterior law

$$q_u\sim N\!\left(0,\ \sigma_p^2\,\frac{n_1\gamma}{n_1\gamma+1}\right).$$

Under pre-announced pricing the firm commits to a plan $\{p_1,p_2\}$. Consumers then play a purchasing game. A set $B\subseteq[0,1]$ of early buyers is an equilibrium if every type in $B$ weakly prefers buying now, $x-p_1\ge 0$ and $x-p_1\ge\delta_c\,\mathbb E[(x+q_u-p_2)^+]$, and every other type weakly prefers to wait. Here $q_u$ has the pre-posterior law for $n_1=|B|$. In period 2 the remaining types buy iff $x+q_u\ge p_2$. The firm's expected profit is

$$\pi_p(p_1,p_2;B)=(p_1-c)\,|B|+(p_2-c)\,\mathbb E\big[\,|\{x\in[0,1]\setminus B:\ x+q_u\ge p_2\}|\,\big],$$

and the optimal pre-announced profit $\pi_p^*$ is its supremum over all plans and all their equilibria. Absence of SL is the same model at $\gamma=0$, where $q_u\equiv 0$.

Formalization targets

Goal: Proposition 3

For $\gamma>0$ there are thresholds $\Delta_{lp}(\gamma)\in(0,1]$ and $\Delta_{hp}(\gamma)\in[0,1)$ such that

$$\delta_c\le\Delta_{lp}(\gamma)\ \text{ or }\ \delta_c\ge\Delta_{hp}(\gamma)\quad\Longrightarrow\quad \pi_p^*\big|_{\gamma}>\pi_p^*\big|_{\gamma=0}.$$

Milestones

1. Lemma 1: the pre-posterior law above.
2. Display (2): without SL, the buyer set is $[\tau(p_1,p_2),1]$ for an explicit threshold $\tau$.
3. Proposition 1: without SL, $\pi^*=(1-c)^2/(\delta_c+3)$, attained at $p_1^*=\tfrac{c(1+\delta_c)+2}{\delta_c+3}$ and $p_2^*=\tfrac{2c+\delta_c+1}{\delta_c+3}$.
4. Lemma 2: with SL, the buyer set is $[\theta,1]$, where $\theta$ solves the implicit equation (3), or $\theta=1$ under adoption inertia. A companion item states that $\theta$ is monotone in $\gamma,p_1,\delta_c,p_2$.
5. Lemma 5: waiting is worth strictly more when more consumers buy early.
6. Proposition 2: adoption inertia is never optimal, and patient consumers face an increasing optimal price path.
7. Examples 1 and 2: with myopic consumers, SL raises the optimal second-period price and the optimal profit.
8. $\pi_p^*$ is continuous in $\delta_c\in[0,1]$.

Significance

Proposition 3 says that social learning helps the firm at both ends of the patience range. For myopic consumers this is the informational effect alone. For patient consumers it holds even though learning makes them strictly more inclined to wait (Lemma 2) and the committed price cannot react to the reviews. The paper's numerical experiments found no intermediate $\delta_c$ at which learning hurts, but the theorem asserts only the two ends. The result underlies the managerial conclusions of the paper: firms gain from encouraging reviews even when consumers are strategic.

The result is proved in the paper; nothing in the model has been machine-checked before. A formal proof would check the equilibrium analysis of a continuum purchasing game with an endogenous information externality. Its intermediate results also serve the paper's two other missions: responsive pricing, and the comparison of responsive with pre-announced pricing. These are the Normal convex-order monotonicity (Lemma 5), the implicit threshold equation (Lemma 2), the no-SL benchmark (Proposition 1) and a Maximum-Theorem continuity statement.

Difficulty

The equilibrium threshold $\theta$ solves an equation whose Normal kernel has a variance that depends on $\theta$ itself. Existence, uniqueness and monotonicity are not closed-form computations.

The endpoint $\delta_c=1$ is the delicate one. There learning makes waiting most attractive, and the strict gain over the no-SL optimum $(1-c)^2/4$ must come from a plan that still induces a positive mass of early buyers.

Continuity of $\pi_p^*$ in $\delta_c$ is a Maximum-Theorem argument for a supremum over an unbounded set of prices whose objective passes through an implicit equilibrium. Compactness of the relevant price set has to be established, not assumed.

Formalization scope

Every statement is taken over the standing assumptions $\sigma_p>0$, $\gamma\ge 0$, $\delta_c\in[0,1]$, $c\in[0,1)$, with firm discount factor $1$ and pure strategies. Further conventions:

• Absence of SL is the same model at $\gamma=0$. There the pre-posterior law is the point mass at $0$, which is the paper's limit $\gamma\to 0$.
• Best responses are weak. Equilibrium buyer sets are therefore unique only up to Lebesgue-null sets. The degenerate plan $p_1=p_2$ at $\delta_c=1$ without SL, where every type is indifferent, is excluded from the uniqueness claim of (2).
• Optimal values are suprema in the extended reals over all real plans and all purchasing equilibria. They are never real suprema with junk values, never the profit at a closed-form price, and never restricted to threshold equilibria. "Optimal plan" means a plan one of whose equilibria attains the supremum.
• Proposition 3's thresholds are stated with the strict bounds $\Delta_{lp}>0$ and $\Delta_{hp}<1$. With closed bounds the claim would follow from the cases $\delta_c=0$ and $\delta_c=1$ alone.
• Added hypotheses, each disclosed in its item:
  • $p_1\in[0,1]$ in Lemma 2 and its monotonicity item, and $p_1\ge 0$ in (2);
  • $\delta_c>0$ in Lemma 5;
  • $p_1<1$ in Example 1 (at $p_1=1$ nobody buys early, so the example's strict inequality fails there), and $c<p_1$ for its no-SL uniqueness part;
  • $\delta_c<1$ for uniqueness in Proposition 1;
  • $n_1>0$ in Lemma 1;
  • existence of an optimal plan, asserted together with Proposition 2(ii);
  • monotonicity of $\theta$ is weak.
• Not posed:
  • Lemma 2(ii) is built into the second-period demand.
  • The "unique equilibrium" clauses of Propositions 1 and 2 are the items for (2) and Lemma 2.
  • The fixed-price variant of Proposition 3 (pp. 17–18) is false at $\delta_c=1$.

The witness used in the printed proof of Proposition 2(i) does not settle the case $\delta_c=1$.

A complete development needs Gaussian expectations of hinge functions and their monotonicity in the variance (strict convex order), an implicit-equation argument for the threshold, and a version of Berge's Maximum Theorem. The Gaussian lemmas and the no-SL benchmark are reusable across the series. Contributions to any milestone are welcome.

Selected references

• Y. Papanastasiou, N. Savva, Dynamic Pricing in the Presence of Social Learning and Strategic Consumers, Management Science 63(4):919–939, 2017. https://doi.org/10.1287/mnsc.2015.2378 (cited from the accepted manuscript MS-14-00028.R2, 2016)
• M. Landsberger, I. Meilijson, Intertemporal price discrimination and sales strategy under incomplete information, RAND Journal of Economics 16(3):424–430, 1985. https://doi.org/10.2307/2555568
• G. P. Cachon, R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3):497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002. https://doi.org/10.1002/9780470317167
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

Motivation

In an aggregative game, each player's decision affects a common quantity, such as total production or total demand. An agent may be able to calculate its own preferred response while lacking direct access to that aggregate. Koshal, Nedić, and Shanbhag study how agents can estimate it by exchanging information only with neighbours on a communication graph. Their asynchronous gossip algorithm lets one randomly selected agent contact a neighbour at each tick; both agents update their estimates and decisions. The constant stepsize regime matters when agents cannot steadily reduce their stepsizes or want to keep responding to new information. It gives an error bound rather than exact convergence: the decisions remain near an equilibrium by an amount controlled by the step, the game, and the graph. The model and this bound are from Koshal, Nedić, and Shanbhag, 2016.

The same paper analyzes a synchronous scheme with diminishing steps and a gossip scheme with update-count steps. This mission isolates the constant-step case in §4.3, and targets the equal-probability, equal-stepsize display at the end of that section. It uses the paper's numbered Lemmas 2, 3, and 11 and relations (30), (31), (44), and (55) as intermediate targets. The restriction to the final special case is material: the argument printed for general player-specific steps and update probabilities has gaps in (53) and (54), while both problematic terms disappear when the steps and update probabilities are equal.

Setting

There are $N$ players, each choosing $x_i$ from a nonempty compact convex set $K_i\subseteq\mathbb R^n$. Write $K=\prod_iK_i$ for feasible profiles and $\bar K=\{\sum_i x_i:x_i\in K_i\}$ for feasible aggregates. Player $i$ has a component map $F_i(x_i,u)$, evaluated at its own decision and an aggregate argument. At a feasible profile $x$, the game map is $\phi(x)_i=F_i(x_i,\sum_jx_j)$. An equilibrium target is the solution $x^*$ of the variational inequality $\operatorname{VI}(K,\phi)$: for every $x\in K$, $\sum_i\langle x_i-x_i^*,\phi(x^*)_i\rangle\ge0$. The paper derives this map from player payoff gradients under its Assumption 1; the present formalization starts with the component maps used by the algorithm.

A connected undirected graph lists the players that may exchange information. At tick $k$, a uniform random player $I^k$ wakes and contacts a neighbour $J^k$ with probability $p_{I^kJ^k}>0$. These draws are independent across ticks. Only the contacted pair average their current estimates $v_i^k$ to obtain $\hat v_i^k$, then project a step using $F_i(x_i^k,N\hat v_i^k)$ onto $K_i$. All agents update their estimate by $v_i^{k+1}=\hat v_i^k+x_i^{k+1}-x_i^k$; for agents outside the pair this leaves both state variables unchanged. The mean estimate is $y^k=N^{-1}\sum_i v_i^k$. Lemma 2 identifies it with the mean decision. The update probability of player $i$ is $p_i=N^{-1}(1+\sum_jp_{ji})$. These definitions and the discrete gossip algorithm are given in §4.1 of the source.

Formalization targets

Constant-step error bound

Suppose $\phi$ is strongly monotone with modulus $\mu>0$, every player uses the same positive step $\alpha$, and all update probabilities equal $p$. Let $C$ bound the gradient evaluations as in Lemma 3. Let $\lambda\in(0,1)$ be a mean-square contraction constant for the gossip matrix $D(k)=W(k)-N^{-1}\mathbf1\mathbf1^\top$, as in (30). If $\bar L_i$ are the aggregate Lipschitz constants of Assumption 3 and $M$ bounds the diameter of each $K_i$, put $B=(\max_i\bar L_i)NM$. Under the inherited assumptions of Proposition 4 and $0<\alpha<1/(2\mu p)$, the goal is existence and uniqueness of $x^*$ together with the last display on PDF page 29:

$$\limsup_{k\to\infty}\mathbb E\|x^k-x^*\|^2 \le \frac{\alpha}{\mu}\left(2C^2N+\frac{BC\sqrt{2nN}}{1-\sqrt\lambda}\right).$$

The milestones separately assert the unique VI solution, the aggregate identity, the bounded gradient evaluations, the contraction estimates (30)–(31), the one-step disagreement relation (44), Lemma 11's limiting disagreement bounds, and the equal-case recursion (55). Together they expose the quantities appearing in the target without weakening its constant or its dependence on $n$ and $N$.

Significance

The bound separates the effects of the step, game regularity, number of agents, decision dimension, and communication quality. In particular, for fixed other parameters the right-hand side scales linearly in $\alpha$ and worsens as $\lambda$ approaches one. It is a quantitative guarantee for a decentralized procedure that sees neighbour messages instead of the exact aggregate. The VI existence and uniqueness target also identifies the equilibrium to which the error is measured. The paper proves the special case in its concluding bound on page 29, subject to the domain correction described below; it is not an unresolved research conjecture.

Formalizing the result produces a reusable interface for graph gossip matrices, random pair draws, relational Euclidean projection, and nonnegative expected disagreement. The intermediate contraction and tracking statements can support other constant-step distributed optimization arguments. The theorem declarations in this proposal are open Lean proof obligations; a successful local build checks their types and definitions, not the mathematical claims. Contributions that establish these obligations, sharpen a bound under the same model, or isolate reusable probability and projection results are in scope.

Difficulty

The estimates $v_i^k$ are coupled to both random pair averaging and the agents' decision changes, so graph connectivity alone does not state a numerical disagreement bound. The proof has to respect the actual distribution of waking and contacted agents when moving from a one-player inequality to an expected profile error. The printed general version illustrates the risk: Assumption 8 controls changes in $x_i$ at a fixed aggregate and therefore cannot justify (53), where the aggregate changes; (54) also replaces coefficients on signed terms by their minimum. The final equal-step, equal-probability case removes these two obstacles, but still requires the exact constants in Lemma 11 and the error recursion.

Formalization scope

Players are indexed by Fin N, decisions use EuclideanSpace ℝ (Fin n), and a profile's squared Euclidean norm is the sum of squared block norms. Coordinate vectors across players also use a Euclidean norm; the ordinary Lean norm on Fin N → ℝ would be a supremum norm. The run starts from a deterministic feasible profile. This fixes the initial state before the independent discrete gossip draws, representing the source's Poisson-clock protocol at its tick times. A projection is a nearest-point relation on a nonempty compact convex set, with no arbitrary value on an empty set. Positive contact probabilities on all graph edges keep the connected graph active.

Assumption 1 is expressed through nonempty compact convex $K_i$ and continuity of $F_i$ on $K_i\times\bar K$, the part of the payoff regularity used by the algorithm. Assumption 3 is stated for every aggregate argument in $\mathbb R^n$, a disclosed strengthening of its printed domain $\bar K$: $N\hat v_i^k$ can leave $\bar K$, as the paper's footnote on page 10 acknowledges. Assumption 8 remains a hypothesis inherited from Proposition 4 even though its term vanishes for equal steps. The constants $C$, $\lambda$, and $M$ carry their defining bounds as hypotheses; the conclusion does not assume Lemma 11 or (55). Expected nonnegative quantities use extended-real lintegrals and an extended-real limit superior, preventing a failed Bochner integral from silently becoming zero. The formalization asserts existence of a VI solution, so an empty solution set cannot trivialize the goal.

Selected references

• J. Koshal, A. Nedić, and U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3):680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501.

Motivation

In an aggregative game, each player's cost depends on its own decision and on the sum of all players' decisions. That form appears in resource sharing, production, and network games: a player may know its own choice while lacking a central feed of the aggregate. A distributed algorithm therefore has to estimate the aggregate through local communication as it updates decisions. Koshal, Nedić, and Shanbhag study this setting and give both synchronous and gossip schemes in Distributed Algorithms for Aggregative Games on Graphs. This mission concerns their asynchronous scheme, in which a random pair communicates at each tick.

The question is whether irregular, local updates still find the game's equilibrium when no agent knows in advance how often it will be selected. Each agent uses its own update count to set its step length. The paper's Proposition 3 states almost-sure convergence under strict monotonicity, compact strategy sets, and a connected graph. The result is a convergence claim about the complete random process, including who wakes, whom they contact, which estimate they exchange, and which projected step they take.

Setting

There are $N\ge1$ agents. Agent $i$ chooses $x_i\in K_i\subseteq\mathbb R^n$, with $K_i$ nonempty, compact, and convex. A strategy profile is $x=(x_1,\ldots,x_N)$ in $K=\prod_i K_i$, and its aggregate is $\bar x=\sum_i x_i$. The map $F_i(x_i,u)$ is the player's first-order response when its own decision is $x_i$ and its aggregate argument is $u$. The game map is $\phi_i(x)=F_i(x_i,\bar x)$. A solution $x^*$ of the variational inequality $\mathrm{VI}(K,\phi)$ is feasible and satisfies

$$\sum_i\langle x_i-x_i^*,\phi_i(x^*)\rangle\ge0 \quad\text{for every }x\in K.$$

The paper obtains $F_i$ from differentiable convex player costs, making VI solutions Nash equilibria. The formal statements take $F_i$ as the primitive map used by the algorithm. Strict monotonicity means $\sum_i\langle\phi_i(x)-\phi_i(y),x_i-y_i\rangle>0$ for different feasible profiles $x,y$. Along with continuity and compact convex strategy sets, it makes the VI solution unique. The paper's Assumptions 1–3 also impose a uniform Lipschitz bound on how $F_i(x_i,u)$ changes with $u$.

Agents occupy a connected, undirected graph. At a discrete tick $k$, a uniformly selected agent $I^k$ contacts a neighbour $J^k$ with probability $p_{I^kJ^k}>0$ on every edge. The ordered pairs are independent across ticks. Each agent maintains an aggregate estimate $v_i^k$; the selected pair average their estimates to form $\hat v_i^k$. Those agents take a projected step using $F_i(x_i^k,N\hat v_i^k)$ and then add their decision change to the estimate. Other agents retain their decisions and estimates. Initially $v_i^0=x_i^0$. The number $\Gamma_k(i)$ counts agent $i$'s updates through tick $k$, and its step length at an update is $\alpha_{k,i}=1/\Gamma_k(i)$. Equations (23)–(29) of the paper define these operations.

Formalization targets

Goal: almost-sure equilibrium convergence

Under Assumptions 1–3 and connectedness of the gossip graph, Proposition 3 asserts that there is a unique $x^*$ solving $\mathrm{VI}(K,\phi)$ and that the generated process satisfies

$$\Pr\bigl(\lim_{k\to\infty}x^k=x^*\bigr)=1.$$

The goal includes existence and uniqueness of $x^*$, rather than conditioning convergence on a possibly nonexistent solution. Its random draws have the rate-one-clock law: $\Pr(I^k=i,J^k=j)=p_{ij}/N$.

Milestones

The five milestones record the VI's unique solution from the proof of Proposition 1, conservation of the agents' average estimate in Lemma 2, the almost-sure stepsize bounds of Lemma 7, their summability consequences in Corollary 1, and the mean-square gossip contraction in relations (30)–(31). They cover the equilibrium, tracking, step length, and network-mixing parts of the claim. Their source wording, indices, and PDF pages are attached to the mission items.

Significance

The result shows that a shared aggregate can be learned well enough through pairwise, random exchanges to reach the same equilibrium characterized by the centralized VI. Update counts permit agents to choose diminishing steps without a common iteration clock or a schedule ensuring equal participation on each finite interval. Connectedness and positive contact probabilities ensure every graph edge can carry information. The convergence assertion is almost sure, so it concerns individual sample paths outside a null set, rather than merely an average error.

Formalizing the result would connect finite graph gossip, random update counts, projected VI iteration, and almost-sure convergence in one reusable development. The paper proves Proposition 3; this mission supplies an open machine-checked target, not a claim that the result is unresolved mathematically. A proof would need honest probability statements for the draw law and summability and a projection interface that does not assign arbitrary values on empty sets. The VI existence and uniqueness milestone can also serve other compact, strictly monotone games.

Difficulty

Pairwise averaging preserves the mean estimate, but it does not make each agent's estimate equal to that mean at every step. A projected decision change immediately perturbs the local estimate again. The selected agents and their step lengths also depend on the same update history, so deterministic simultaneous-update arguments do not directly apply. The paper controls this interaction using update-count asymptotics, contraction of the random gossip matrix, and almost-sure summability. None of those conclusions follows from connectedness alone if a nominal edge has zero contact probability.

Formalization scope

Lean represents each decision in EuclideanSpace ℝ (Fin n) and profiles as functions on Fin N. The aggregate is a finite sum. A projection is the relation saying that the selected point lies in its set and minimizes Euclidean distance, rather than a total function with an arbitrary output on an empty set. The profile topology used for convergence is the finite product topology. For vectors indexed by agents, relations (30)–(31) use the explicit Euclidean coordinate norm; the default norm of Fin N → ℝ is a sup norm.

The continuous-time Poisson clocks are encoded through their induced independent discrete tick pairs and exact joint law. Initial decisions are fixed and feasible. The source allows random initial decisions; the formal goal covers every deterministic start. This restriction is recorded because the paper's stated random initialization would require an explicit independence relation with future clock draws. Tick indices start at zero in Lean; a selected agent has $\Gamma_k(i)\ge1$, so the value assigned to $1/0$ never drives an update. The positive-time series and bounds still begin at $k=1$.

The paper gives the Lipschitz condition on aggregate arguments only in the feasible aggregate set $\bar K$. Its algorithm can evaluate $F_i$ outside that set, as its own footnote acknowledges. This development explicitly extends that condition to all of $\mathbb R^n$ to make those evaluations controlled. The change is substantive and disclosed on each affected item; the preprint's Lemma 3 proof contains the corresponding domain gap. The goal assumes neither the stepsize estimates nor the network contraction nor convergence of the estimate errors; they remain mathematical work. Further contributions may formalize the omitted intermediate lemmas, or refine the initialization and domain assumptions while preserving a meaningful statement.

Selected references

• J. Koshal, A. Nedić, and U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3), 680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501.

Motivation

In an aggregative game, a player's cost depends on its own decision and on a summary of all players' decisions. An electricity producer, for example, may choose its output while the market price depends on total output. When players communicate only with neighbours, each player must estimate the aggregate before making an update. Koshal, Nedić, and Shanbhag study this setting with communication links that can change over time, and prove convergence of a synchronous algorithm using only local messages Koshal–Nedić–Shanbhag, 2016.

The mission targets Proposition 2 of the pinned preprint. It treats the algorithm itself as a mathematical object: the claim must hold for every sequence satisfying its graph, weight, stepsize, and projected update conditions. The result addresses a concrete information constraint. Players cannot read the true aggregate while the algorithm runs; they have individual estimates constructed from their neighbours' estimates.

Setting

There are $N\ge1$ players. Player $i$ chooses $x_i\in K_i\subseteq\mathbb R^n$, with each $K_i$ nonempty, compact, and convex. Write $x=(x_i)_i$, $K=\prod_i K_i$, and $\bar x=\sum_i x_i$. The attainable aggregate set is $\bar K=\{\sum_i x_i:x\in K\}$. A map $F_i(x_i,u)$ gives the component of the game's gradient field at player $i$'s decision and aggregate argument $u$. Its profile field is $\phi_i(x)=F_i(x_i,\bar x)$.

The target point is a solution of the variational inequality $\operatorname{VI}(K,\phi)$: it belongs to $K$ and satisfies

$$\sum_{i=1}^N (x_i-x_i^*)^\top\phi_i(x^*)\ge0\qquad\text{for every }x\in K.$$

The paper obtains this field from differentiable player costs. The convergence theorem is stated for the field and the VI, while the connection to a Nash equilibrium is established separately in Proposition 1 Koshal–Nedić–Shanbhag, pp. 4–6. Strict monotonicity of $\phi$ on $K$ says that $(\phi(x)-\phi(x'))^\top(x-x')>0$ whenever feasible $x\ne x'$. Together with compactness and continuity, this yields the unique VI solution used in the target.

At time $k$, player $i$ keeps a decision $x_i^k$ and an estimate $v_i^k$ of the average decision, initially $v_i^0=x_i^0$. A matrix $W(k)=(w_{ij}(k))$ mixes estimates along an undirected communication graph. Each row and column of $W(k)$ sums to one; non-neighbours receive zero weight, while every neighbour and the player itself receive at least $\delta>0$. The union of the communication graphs over any $Q\ge1$ consecutive times is connected. The local aligned estimate and the two updates are

$$\hat v_i^k=\sum_j w_{ij}(k)v_j^k,\qquad x_i^{k+1}=\Pi_{K_i}\bigl[x_i^k-\alpha_k F_i(x_i^k,N\hat v_i^k)\bigr],\qquad v_i^{k+1}=\hat v_i^k+x_i^{k+1}-x_i^k.$$

Here $\Pi_{K_i}$ denotes Euclidean nearest-point projection. The stepsizes $\alpha_k$ decrease, their sum diverges to $+\infty$, and their squares are summable. The paper calls these graph, weight, and stepsize conditions Assumptions 4–6 Koshal–Nedić–Shanbhag, pp. 7–9.

Formalization targets

Unique VI solution

The first milestone makes the existence and uniqueness statement used in the proof explicit:

$$\exists!x^*\in K:\quad(x-x^*)^\top\phi(x^*)\ge0\quad\text{for all }x\in K.$$

The other milestones follow the paper's numbered Lemmas 1–4 and 6 and its displayed relations (19)–(20). They state that the mean of the players' estimates is the true mean decision, that the matrix products mix geometrically, that the relevant gradients and estimate errors are controlled, and that the weighted estimate errors have finite total sum Koshal–Nedić–Shanbhag, pp. 9–14.

Proposition 2

For every synchronous run under Assumptions 1–6, the goal asserts both a unique VI solution and convergence of the whole decision sequence:

$$\exists!x^*\in K\text{ solving }\operatorname{VI}(K,\phi), \qquad x^k\longrightarrow x^*.$$

The target is a qualitative convergence result. It does not prescribe a convergence rate for $x^k$ Koshal–Nedić–Shanbhag, Proposition 2, p. 13.

Significance

The theorem says that local estimate mixing is sufficient for every player's projected gradient decision to approach the same equilibrium, even when the communication graph changes, provided connectivity recurs within a fixed window. The result gives a precise condition under which access to the aggregate can be replaced by neighbour messages. Its milestone on the matrix products supplies an explicit estimate for how information spreads; the summability milestones connect that estimate to the optimization error.

The paper contains a mathematical proof, but this mission's Lean declarations are open statements with sorry bodies. A completed formalization would turn the paper's VI existence, mixing, projection, and convergence arguments into individually reusable verified results. The general product-set VI and nearest-point relation are separated from the paper's particular synchronous model so later developments can use them without importing graph-specific definitions.

Difficulty

The obvious single-agent projected-gradient argument assumes each update uses $F_i(x_i^k,\bar x^k)$. Here it uses $F_i(x_i^k,N\hat v_i^k)$ instead, and the estimate errors depend on a changing product of weight matrices. Connectivity of each individual graph is not assumed, so a one-step contraction statement is unavailable. The proof must control time-varying mixing and accumulate its error without losing convergence. Strict monotonicity then identifies the limit, but it does not by itself bound the transient disagreement.

The printed hypotheses also leave a domain issue. The algorithm evaluates $F_i$ at $N\hat v_i^k$, which need not lie in $\bar K$; the paper's footnote on p. 10 acknowledges that $\hat v_i^k$ may leave its apparent feasible aggregate region. The printed Lipschitz condition covers only $\bar K$, so the target explicitly requires it for all aggregate arguments. The printed Lemma 3 also gives only unit column sums, which allow arbitrarily large negative and positive entries; its mission item carries the graph and positive-weight assumptions needed for the bound. These changes are recorded in the item notes and in the source analysis Koshal–Nedić–Shanbhag, pp. 7–10.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin n) and players in Fin N; Lean player zero is the paper's player one. A profile is a finite function, and its squared Euclidean norm is the sum of the squared norms of its blocks. The conclusion uses the equivalent finite product topology. The variational inequality's inner product is written as a sum over players, avoiding the sup norm carried by a Lean function space. Graphs are undirected SimpleGraphs; self-neighbours are included explicitly. The product $\Phi(k,s)$ places the newest matrix on the left. Projection is a relation requiring a genuine nearest point in $K_i$, rather than a total function with an arbitrary value on an empty set.

The target fixes $N\ge1$, $\delta>0$, and nonempty $K_i$. It uses continuity of $F_i$ on $K_i\times\bar K$ as the field-level part of Assumption 1, and the extended all-$\mathbb R^n$ form of Assumption 3 stated above. The stepsize sum is represented by partial sums tending to $+\infty$, and $\sum_k\alpha_k^2<\infty$ by summability. Existence and uniqueness are part of the goal conclusion; no bound on the gradients or summability of the estimate error is assumed by the goal. A complete development needs reusable compact-product VI existence, Euclidean projection facts, matrix-product mixing for changing graphs, finite-dimensional norm estimates, and real-series convergence. Contributions proving these milestones and their intermediate lemmas are welcome.

Selected references

• J. Koshal, A. Nedić, U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3):680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501. This mission cites the pinned arXiv page indices.