Algorithmic Game Theory

Motivation

Mean-field games describe large populations of identical agents who interact only through the distribution of their states. Each agent solves a stochastic control problem in which the population appears through a deterministic flow of distributions, and an equilibrium requires that this flow coincide with the distribution the agents generate themselves. The theory goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007) in continuous time. In discrete time, Saldi, Başar and Raginsky (SIAM J. Control Optim. 2018) proved existence of equilibria for risk-neutral agents with discounted costs on Polish state spaces.

Risk-neutral agents care only about expected cost. Many applications in engineering and finance call for agents that also penalize the variability of their cost. A standard way to model this is the exponential (risk-sensitive) criterion $E[\exp(\lambda\cdot\text{cost})]$ with risk factor $\lambda>0$. Its theory for single-agent Markov decision processes goes back to Howard and Matheson (1972) and Jacobson (1973), and Bäuerle and Rieder (Math. Oper. Res. 2014) treat general utilities. Saldi, Başar and Raginsky (arXiv:1808.03929, Math. Oper. Res. 2020) carry the discrete-time mean-field program over to this criterion. This mission covers its first main result: existence of a mean-field equilibrium (Theorem 1).

Setting

The state space $\mathsf X$ and the action space $\mathsf A$ are Polish, and $\mathsf A$ is compact. $\mathcal P(E)$ denotes the probability measures on $E$, with the topology of weak convergence and its Borel σ-field. The model consists of:

• a stochastic kernel $p(\cdot\,|\,x,a,\mu)$ on $\mathsf X$ given $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$;
• a one-stage cost $c(x,a,\mu)\in[0,K]$;
• an initial law $\mu_0$, a discount factor $\beta\in(0,1)$ and a risk factor $\lambda>0$.

A Markov policy is a sequence $\pi=(\pi_t)_{t\ge0}$ of kernels $\pi_t(da\,|\,x)$. A policy in general is allowed to depend on the whole history $(x(0),a(0),\dots,x(t))$. Given a measure flow $\mu=(\mu_t)_{t\ge0}\subset\mathcal P(\mathsf X)$, a generic agent evolves as

$$x(0)\sim\mu_0,\qquad a(t)\sim\pi_t(\cdot\,|\,\text{history}),\qquad x(t+1)\sim p(\cdot\,|\,x(t),a(t),\mu_t),$$

and pays the risk-sensitive cost

$$J_\mu(\pi)=E^\pi\Big[\exp\Big(\lambda\sum_{t=0}^\infty\beta^tc(x(t),a(t),\mu_t)\Big)\Big].$$

For a Markov policy, $\Lambda(\pi)$ is the flow of state laws it generates: it starts at $\mu_0$ and satisfies $\mu_{t+1}(\cdot)=\int p(\cdot\,|\,x,a,\mu_t)\,\pi_t(da|x)\,\mu_t(dx)$. A pair $(\pi,\mu)$ is a mean-field equilibrium if $\mu=\Lambda(\pi)$ and $\pi$ minimizes $J_\mu$ over all policies.

Assumption 1 asks for the following:

• (a) $c$ is continuous with $\|c\|\le K$;
• (b) $p$ is weakly continuous in $(x,a,\mu)$;
• (c) $\mathsf A$ is compact;
• (d) there are $\alpha\ge0$ and a continuous moment function $w\ge1$ (compact sets $K_n\uparrow\mathsf X$ with $\inf_{x\notin K_n}w(x)\to\infty$) with $\int w(y)\,p(dy|x,a,\mu)\le\alpha w(x)$;
• (e) $\int w\,d\mu_0<\infty$.

Formalization targets

Goal: Theorem 1 (p. 10)

Under Assumption 1 there are a Markov policy $\pi$ and a flow $\mu$ with

$$\mu=\Lambda(\pi)\qquad\text{and}\qquad J_\mu(\pi)=\inf_{\sigma\in\Pi}J_\mu(\sigma).$$

Milestones

In the paper's order of proof:

1. Proposition 1: Markov policies achieve the optimal value.
2. Lemmas 1–3: the finite- and infinite-horizon optimal value functions $J^n_k(\cdot,\lambda\beta^k)$ and $J_k(\cdot,\lambda\beta^k)$ of the nonhomogeneous MDP of a fixed flow are bounded and continuous. They satisfy the dynamic programming equation $T_kJ_{k+1}(\cdot,\lambda\beta^{k+1})=J_k(\cdot,\lambda\beta^k)$, and

$$\big\|J^n_k(\cdot,\lambda\beta^k)-J_k(\cdot,\lambda\beta^k)\big\|\le\frac{\lambda K}{1-\beta}e^{\frac{\lambda\beta^kK}{1-\beta}}\beta^{n+1}.$$

3. Theorem 2: a Markov policy is optimal if and only if it almost surely selects minimizers in the dynamic programming equation.
4. Propositions 2–5 and Lemma 4: equilibria are fixed points of a set-valued map $\Gamma$ on state–action flows in $\Xi=\prod_t\{\nu:\nu_1(w)\le\alpha^tM\}$; the optimal value functions depend continuously on the flow; and the graph of $\Gamma$ is closed in $\Xi\times\Xi$.

Significance

The result. Theorem 1 is what makes the second main result of the paper meaningful. That result, Theorem 3 and the second mission of this series, states that the equilibrium policy is an $\varepsilon$-Markov–Nash equilibrium of every $N$-agent game with $N$ large enough. Equilibria of finite risk-sensitive games with many agents are rarely computable, so a mean-field equilibrium gives an approximately optimal decentralized policy that ignores the other agents' states. Along the way, the paper proves results on nonhomogeneous risk-sensitive MDPs that it describes as "mostly absent and dispersed in the literature": uniform finite-to-infinite horizon bounds and a characterization of optimal Markov policies. These results are useful outside game theory.

Formalizing it. The result is proved on paper. No part of it, nor of the risk-neutral precursor, has a machine-checked proof. Formalization produces a verified theory of nonhomogeneous risk-sensitive MDPs on Polish spaces, a verified closed-graph argument for the mean-field map, and an exact record of the hypotheses. The paper omits or cites several steps: Proposition 1, Proposition 2, Lemma 2, the conditional optimality (8) and the nonemptiness and convexity of $\Gamma(\nu)$. A formalization has to supply them.

Difficulty

The obvious route is Banach's fixed point theorem for the dynamic programming operator, as in risk-neutral discounted MDPs. It fails here: the cost is multiplicative, and the operator $T_k$ is not a contraction. Uniform convergence of value iteration has to come from the explicit tail bound of Lemma 3 instead.

The second obstacle is the fixed point itself. The natural map, from a flow to the flows of its optimal policies, is set-valued and lives on an infinite product of spaces of measures. Kakutani–Fan–Glicksberg applies only after three steps:

• re-encoding the problem on state–action flows (the map $\Gamma=C\cap B$);
• proving compactness of $\Xi$ through the moment function (tightness);
• proving that the graph of $\Gamma$ is closed (Proposition 4).

The last step requires the optimal value functions to vary continuously with the flow (Proposition 5) and a portmanteau argument for sets defined by optimality conditions. None of this machinery (the Kakutani–Fan–Glicksberg theorem in locally convex spaces, Prokhorov compactness via moment functions, continuous convergence) is in Mathlib in the required form.

Formalization scope

$\mathcal P(E)$ is a type synonym of Mathlib's ProbabilityMeasure E with the weak topology and its Borel σ-field. The kernel $p$ is a Mathlib Kernel on $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$. Policies are sequences of Markov kernels, and history-dependent policies take $(\mathsf X\times\mathsf A)^t\times\mathsf X$ as input. The law $P^\pi$ is built with the Ionescu–Tulcea kernel Kernel.trajMeasure, one coordinate $(x(t),a(t))$ per time step. Time is $0$-based.

Standing hypotheses on every statement:

• $\mathsf X$ and $\mathsf A$ are Polish and Borel;
• $\mathsf A$ is compact and nonempty (used tacitly by the paper);
• $\beta\in(0,1)$, $\lambda>0$, and $c\ge0$ is measurable;
• Assumption 1.

For §4.2 the pair $(\alpha,w)$ defining $\Xi$ is an explicit argument. In §4.1, "policy" means Markov policy, as the paper states on p. 11. The conditional expectations "given $x(k)=x$" are expectations for the chain started at time $k$ in $x$. Lemma 1 is stated with $\zeta_{k,n}=\sum_{t=k}^n\beta^t$, the quantity its proof uses; the page prints $\sum_{t=k}^n\beta^k$.

The goal asks for a Markov equilibrium policy that is optimal against all history-dependent policies, at least as strong as Definition 3. Optimality is "$\le$ the cost of every policy", not an infimum, so it has no junk case. The cost is a genuine integral: with $c\ge0$ bounded, the integrand lies in $[1,e^{\lambda K/(1-\beta)}]$, so no policy is trivially optimal. The moment-function predicate has no infimum, so compact $\mathsf X$ is admitted.

Contributions are welcome at every level:

• risk-sensitive dynamic programming on Borel spaces (reusable for any MDP);
• the Kakutani–Fan–Glicksberg theorem in locally convex spaces;
• Prokhorov compactness from moment functions;
• measurable selection and disintegration of state–action measures.

Selected references

• N. Saldi, T. Başar, M. Raginsky, Discrete-time Risk-sensitive Mean-field Games, arXiv:1808.03929v2, 2018; published as Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games, Math. Oper. Res. 45(4), 2020. https://arxiv.org/abs/1808.03929
• N. Saldi, T. Başar, M. Raginsky, Markov–Nash Equilibria in Mean-Field Games with Discounted Cost, SIAM J. Control Optim. 56(6), 2018. https://doi.org/10.1137/17M1112583
• N. Bäuerle, U. Rieder, More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014. https://doi.org/10.1287/moor.2013.0601
• O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0
• C. D. Aliprantis, K. C. Border, Infinite Dimensional Analysis, 3rd ed., Springer, 2006. https://doi.org/10.1007/3-540-29587-9

Motivation

Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the $n$-player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?

The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.

Setting

Let $G$ be a finite simple graph on vertex set $\{1,\dots,n\}$ with adjacency matrix $A_G$ and degree matrix $D_G$. Its Laplacian is $L_G = D_G^{-1}A_G - I$. $G$ is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree $\delta(G)$, and $L_G$ is then symmetric with eigenvalues $\lambda^G_1,\dots,\lambda^G_n\in[-2,0]$. The empirical eigenvalue distribution is $\mu_G = \frac1n\sum_i\delta_{\lambda^G_i}$.

Fix a horizon $T>0$, a volatility $\sigma>0$ and a weight $c>0$. Player $v$ controls the state

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

driven by independent Brownian motions, with Markovian feedback controls $\alpha_v$, and pays

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

On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with $Q_G(x) = \det(I - xL_G)^{1/n}$ and $f_G$ the solution of $f_G' = c\,Q_G'(f_G)$, $f_G(0) = 0$ on $[0,T]$, the feedback is $\alpha^G_i(t,\boldsymbol x) = -e_i^\top P_G(t)\boldsymbol x$ with $P_G(t) = -f_G'(T-t)L_G(I - f_G(T-t)L_G)^{-1}$. The resulting equilibrium state process $\boldsymbol X^G$ is Gaussian, and the value is $\mathrm{Val}(G) = \frac1n\sum_v J_v$.

For a probability measure $\mu$ define $Q_\mu(x) = \exp\int_{[-2,0]}\log(1-x\lambda)\,\mu(d\lambda)$, so that $Q_{\mu_G} = Q_G$.

Formalization targets

Goal: Theorem 2.6

Let $(G_n)$ be finite transitive graphs without isolated vertices, $|G_n|\to\infty$, with $\boldsymbol X^{G_n}(0) = 0$, and suppose $\mu_{G_n}\to\mu$ weakly for a probability measure $\mu$. Then (1) the ODE $f_\mu' = c\,Q_\mu'(f_\mu)$, $f_\mu(0) = 0$ has a unique solution on $[0,T]$; (2) for every vertex sequence $k_n$ and $t\in[0,T]$,

$$\mathrm{Law}\big(X^{G_n}_{k_n}(t)\big)\to\mathcal N\big(0,V_\mu(t)\big),\qquad V_\mu(t) = \sigma^2\int_0^t\int_{[-2,0]}\Big(\frac{1-\lambda f_\mu(T-t)}{1-\lambda f_\mu(T-s)}\Big)^2\mu(d\lambda)\,ds;$$

(3) the empirical measure $\frac1{|G_n|}\sum_i\delta_{X^{G_n}_i(t)}$ converges weakly in probability to $\mathcal N(0,V_\mu(t))$; (4)

$$\lim_{n\to\infty}\mathrm{Val}(G_n) = -\frac{\sigma^2}2\log\int_{[-2,0]}\frac{-\lambda}{1-\lambda f_\mu(T)}\,\mu(d\lambda).$$

Milestones

The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of $f_\mu$ in $\mu$ (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of $f_\mu$ (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.

Significance

Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs $\mu = \delta_{-1}$ and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, $\mu$ is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.

The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.

Difficulty

Parts (2) and (4) follow from the finite-graph formulas once $f_{G_n}\to f_\mu$ uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.

Formalization scope

The Lean development lives in namespace GraphLQGame.Asymptotics.

• Vertices $\{1,\dots,n\}$ are Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with $N_k\to\infty$.
• $L_G$ is the random-walk Laplacian above, not Mathlib's lapMatrix. $\mu_G$ is built from the real roots of the characteristic polynomial of $L_G$, with multiplicity.
• Weak convergence of measures on $\mathbb R$ is convergence of $\int h\,d\mu_k$ for every bounded continuous $h$. Weak convergence in probability of the empirical measure is convergence in probability of $\int h\,dm^{G_n}(t)$ for every bounded continuous $h$.
• A state process is a pathwise strong solution of (2.1) on its own probability space, driven by a standard Brownian motion and adapted to its completed filtration. Statements about several graphs are statements about laws.
• Costs are $[0,\infty]$-valued lower integrals; the value is computed after asserting finiteness.
• In $P_G$, $f_G'(T-t)$ is written as its ODE value $c\,Q_G'(f_G(T-t))$. ODE solutions are constrained on $[0,T]$ (or on $\mathbb R_+$ for Propositions 3.2 and 3.3), with uniqueness stated on that domain.
• The Gaussian law $\mathcal N(0,V)$ is gaussianReal 0 V.toNNReal; $V_\mu(t)\ge0$.

The goal quantifies over every solution $f_{G_n}$, $f_\mu$ and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for $u = v$, where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.

Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.

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; published in Math. Oper. Res., 2022, https://doi.org/10.1287/moor.2021.1179. 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
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 3.20, Gaussian Poincaré inequality). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• 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

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