All missions

Motivation

A prophet inequality compares the value obtained by an online decision maker with the largest value in a sequence that could be chosen by someone who sees the entire sequence. The online decision maker observes values one at a time and must decide whether to accept the current value before seeing future values. When the common distribution of the values is known, that distribution can inform the stopping rule. This mission concerns the case in which the distribution is unknown and the rule receives no advance samples. The restriction is operational: the same rule must work across every possible common distribution of the observations. Correa, Dütting, Fischer and Schewior show that the familiar $1/e$ success scale of the classical secretary problem is the sharp asymptotic limit for this setting.

The result matters to online selection when historical observations are unavailable. It says that the loss from not knowing the distribution cannot be removed merely by choosing a more elaborate rule based on the values seen so far. It identifies an asymptotic ceiling that applies to every randomized stopping rule, including rules that react to exact numerical values rather than only to their ranks. The paper also studies what changes when samples are supplied; this mission isolates its zero-sample upper bound. The source paper states the result as Theorem 2 on page 6 of arXiv:1811.06114v2.

Setting

Fix a horizon $n\ge1$. Independent observations $X_1,\ldots,X_n$ have the same unknown law $F$ on the nonnegative real numbers. A $(k,n)$ stopping rule first receives $k$ independent samples from that law and then sees the $n$ observations in order. At time $i$, the rule returns a number $r_i\in[0,1]$. This is its conditional probability of stopping on $X_i$, given the samples, the observed prefix $X_1,\ldots,X_i$, and the fact that it has not already stopped. A rule with $k=0$ has no preliminary samples. Its behavior may depend on every observed value and may be randomized.

For fixed samples $s$ and observed values $x$, the conditional probability that the rule stops at $i$ is

$$\Pr(\tau=i\mid s,x) =\left(\prod_{j<i}(1-r_j(s,x_1,\ldots,x_j))\right) r_i(s,x_1,\ldots,x_i).$$

If it never stops, its payoff is $X_\infty=0$. The benchmark is the prophet's maximum $M_n=\max_{1\le i\le n}X_i$. A rule has approximation guarantee $\alpha$ when $\mathbb E_F[X_\tau]\ge\alpha\mathbb E_F[M_n]$ for every allowed law $F$. The paper uses this model in §2, page 5, and develops the zero-sample upper bound in §3.2, pages 6–8. Correa et al.

Two restrictions of a rule appear in the supporting results. A rule is order oblivious when rearranging distinct, nonnegative values seen before the current observation does not change its current stopping probability. A rule is $\varepsilon$ value oblivious on a set $V$ when, on histories of distinct values from $V$ whose current value exceeds the earlier values, its stopping probability at time $i$ lies in $[q_i-\varepsilon,q_i+\varepsilon)$ for some $q_i\in[0,1]$. The $q_i$ depend on the time, while the interval works for every qualifying history in $V$. These are Definitions 1 and 2 of the paper. Correa et al.

Formalization targets

The central target is the paper's Theorem 2. For every tolerance $\delta>0$, a single threshold $n_0$ works for all sufficiently long horizons and all zero-sample rules:

$$\forall\delta>0\ \exists n_0\ \forall n\ge n_0\ \forall r\ \exists F: \quad \mathbb E_F[M_n]>0, \qquad \mathbb E_F[X_\tau]\le (e^{-1}+\delta)\mathbb E_F[M_n].$$

The adversarial law $F$ is chosen after the rule $r$; the threshold $n_0$ depends only on $\delta$. The positive benchmark makes the ratio meaningful. The law in the formal target has finite support, as does the law constructed in the paper's proof.

The milestones follow the paper's stated results and displayed bounds. Lemma 2 supplies an order-oblivious rule with the same guarantee; Lemma 3 is the infinite Ramsey statement used for an infinite monochromatic set; and Lemma 1 supplies an $\varepsilon$ value-oblivious rule on an infinite set. Equation (1) bounds the expected maximum for the paper's hard distribution. The pointwise display before equation (5) bounds the effect of replacing an approximately value-oblivious rule by a record rule. Equation (4) gives the asymptotic secretary upper bound for that record rule. In the formal statements, the $o(1)$ terms in (1) and (4) have explicit finite-horizon or $\forall\delta\,\exists n_0$ meanings. Correa et al., pp. 6–10

Significance

The theorem establishes a ceiling on the worst-case approximation ratio of any zero-sample rule. Its quantifier order matters: a rule may perform well on particular distributions, yet no single rule can exceed $1/e$ uniformly over all unknown distributions for large $n$. Together with the paper's $1/e$ lower bound in Theorem 1, it identifies the sharp asymptotic guarantee without samples. It also gives a baseline against which the paper measures the value of additional samples. Correa et al., Theorems 1–2

The mathematical result is proved in the source paper; the work here is to give a machine-checkable statement and a decomposition that can support a Lean proof. The reusable pieces include a finite-law stopping model, exact conditional stopping probabilities, order and value obliviousness, a uniform-permutation success probability, and an infinite Ramsey statement. The theorem statements in this proposal remain open proof goals. Their compilation checks the representation and syntax, not their truth; solvers must still provide proofs.

Difficulty

The stopping rule class is large. Each $r_i$ can use the exact numerical values of all observations seen so far, and those values range over a continuum. The standard secretary bound concerns decisions based on relative ranks, so it does not immediately bound a value-dependent rule. The upper bound must apply to every such rule while allowing the adversarial distribution to depend on it. A finite hard distribution also produces repeated observations with positive probability, whereas the rank comparison that motivates the secretary bound is simplest on distinct observations. The milestones expose both issues as precise statements without building them into the goal as assumptions. Correa et al., §3.2–3.3

Formalization scope

Lean represents values by real numbers and laws by a finite support in $[0,\infty)$ with nonnegative masses summing to one. Expectations are finite sums over independent product weights. This finite-law class strengthens the existential law in Theorem 2 and restricts the distribution-uniform guarantees in Lemmas 1 and 2; the paper's upper-bound construction has finite support. The rules themselves are arbitrary real-valued functions on real sample and observation vectors, with outputs in $[0,1]$. They are not limited to deterministic, threshold, rank-based, or measurable rules. Indices start at zero in Lean, so Lean index $0$ is the paper's time $1$. Failure to stop has payoff zero.

The positive-benchmark clause $\mathbb E_F[M_n]>0$ rules out the point mass at zero, which would satisfy the printed existential inequality as $0\le0$ for every rule and make the target empty of content. For the same reason, the formalization uses the actual expectation of the maximum and the actual expectation selected by the rule, rather than stipulating a closed-form success bound. A set $V:\mathrm{Set}\;\mathbb N$ may contain zero in Lean, though the paper denotes positive integers by $\mathbb N$; infinitude is unchanged by that one extra point. The paper's Definition 2 prints $r_i$ where its quantified time is $j$; the formalization uses $r_j$. The hard instance and record rule are defined from their parameters, not supplied as unrelated variables. The convention for a zero-length maximum is Lean's real supremum default, but the hard-instance bound explicitly requires $n\ge1$.

A complete development can use Mathlib's finite sums, finite products, permutations, real exponential, and finite-set machinery. The stochastic model and its obliviousness predicates can be reused for sample-complexity variants; the Ramsey theorem is useful independently. Contributions proving the listed milestones, strengthening the finite-law model to broader distributions, or connecting the record-rule bound to an existing secretary formalization are within scope.

Selected references

• José Correa, Paul Dütting, Felix Fischer and Kevin Schewior, Prophet Inequalities for I.I.D. Random Variables from an Unknown Distribution, arXiv:1811.06114v2, 2021; published in Mathematics of Operations Research, 2022. arXiv preprint

Motivation

A correlated equilibrium (Aumann, 1974) is a profile of strategies chosen by a mediator: the mediator draws a joint recommendation from a known distribution, tells each player only their own component, and no player can lower their expected cost by systematically deviating from what they are told. Correlated equilibria contain the Nash equilibria, are computable by linear programming in finite games, and model situations with a coordinating device such as a traffic authority or a market designer.

Mean field games (Lasry–Lions, Huang–Malhamé–Caines, 2006) describe Nash equilibria of games with a large number of symmetric players who interact only through the empirical distribution of their states. The limit model replaces the $N$ players by one representative player facing a flow of distributions. Campi and Fischer (arXiv:2004.06185) ask what the corresponding limit object is for correlated equilibria. Their answer is the correlated mean field game solution: a joint law of a recommendation and a random flow of measures, which, unlike a Nash mean field equilibrium, need not be deterministic. They prove that this notion is the right one in both directions: limits of $N$-player correlated equilibria are correlated solutions (Theorem 6.1), and every correlated solution is approximated by $N$-player approximate correlated equilibria (Theorem 7.1). This mission targets Theorem 6.1.

Setting

Fix a horizon $T\in\mathbb N$, nonempty finite sets $\mathcal X$ (states) and $\Gamma$ (actions), and the noise space $\mathcal Z=[0,1]$ with the uniform law $\nu$. $\mathcal P(\mathcal X)$ is the simplex of probability vectors on $\mathcal X$ with $\mathrm{dist}(m,\tilde m)=\frac12\sum_x|m(x)-\tilde m(x)|$. The model data are a system function $\Psi(t,x,m,a,z)\in\mathcal X$, a running cost $f(t,x,m,a)$ and a terminal cost $F(x,m)$, with $\Psi$ measurable and $f,F$ bounded and measurable.

A restricted strategy is a map $\varphi:\{0,\dots,T-1\}\times\mathcal X\to\Gamma$; their finite set is $\mathcal R$. A strategy modification is any map $u:\mathcal R\to\mathcal R$.

The $N$-player game. Given an initial law $\mathfrak m^N$ on $\mathcal X^N$ and a correlated profile $\gamma^N\in\mathcal P(\mathcal R^N)$, the mediator draws $(\Phi_1,\dots,\Phi_N)\sim\gamma^N$, independently of the initial states and of i.i.d. noises $\xi_j(t)\sim\nu$. Player $j$ moves by

$$X_j(t+1)=\Psi\big(t,X_j(t),\mu_j(t),\Phi_j(t,X_j(t)),\xi_j(t+1)\big),\qquad \mu_j(t)=\tfrac1{N-1}\textstyle\sum_{l\neq j}\delta_{X_l(t)},$$

except that a deviating player $i$ uses $u\circ\Phi_i$ instead of $\Phi_i$. Its cost $J_i^N(\mathfrak m^N,\gamma^N,u)$ is the expected sum of running costs plus terminal cost. $\gamma^N$ is an $\varepsilon$-correlated equilibrium if $J_i^N(\mathfrak m^N,\gamma^N,\mathrm{Id})\le J_i^N(\mathfrak m^N,\gamma^N,u)+\varepsilon$ for all $i$ and $u$, and symmetric if it is invariant under permutations of the players.

The mean field game. A correlated flow is $\rho\in\mathcal P(\mathcal R\times\mathcal P(\mathcal X)^{T+1})$. The representative player starts from $X(0)\sim\mathfrak m_0$, receives $\Phi$ jointly with a random flow $\mu=(\mu(0),\dots,\mu(T))$, $(\Phi,\mu)\sim\rho$, independent of $X(0)$ and of the noises, and moves by $X(t+1)=\Psi(t,X(t),\mu(t),u\circ\Phi(t,X(t)),\xi(t+1))$ with cost $J(\mathfrak m_0;\rho,u)$. $\rho$ is a correlated solution with initial distribution $\mathfrak m_0$ (Definition 4.1) if

1. optimality: $J(\mathfrak m_0;\rho,\mathrm{Id})\le J(\mathfrak m_0;\rho,u)$ for every $u$;
2. consistency: with $u=\mathrm{Id}$, $\mu(t)(\cdot)=\mathbb P\big(X(t)\in\cdot\mid\mu(0),\dots,\mu(T)\big)$ for every $t$.

Formalization targets

Goal: Theorem 6.1

Assume (A1) $\nu\{z:\Psi(t,x,m,a,z)\neq\Psi(t,x,\tilde m,a,z)\}\le w(\mathrm{dist}(m,\tilde m))$ for a measurable $w:[0,\infty)\to[0,1]$ with $w(s)\to0$ as $s\to0^+$, and $\Psi(t,\cdot)$ is $\tau\otimes\nu$-a.e. continuous for every probability $\tau$ on $\mathcal X\times\mathcal P(\mathcal X)\times\Gamma$; (A2) $f,F$ continuous; (A3) $\gamma^N$ is a symmetric $\varepsilon_N$-correlated equilibrium with initial law $\mathfrak m^N$; (A4) $\varepsilon_N\to0$; (A5) $\mathfrak m^N=\otimes^N\mathfrak m_{0,N}$ with $\mathfrak m_{0,N}\to\mathfrak m_0$. Let

$$\rho^N=\mathbb P\circ\big(\Phi_1,\mu_1(0),\dots,\mu_1(T)\big)^{-1},\qquad N\ge2,$$

computed with $u=\mathrm{Id}$. Then

$$\{\rho^N\}_{N\ge2}\ \text{is relatively compact in }\mathcal P(\mathcal R\times\mathcal P(\mathcal X)^{T+1}),\qquad \rho^{N_k}\to\rho\ \Longrightarrow\ \rho\ \text{is a correlated solution}.$$

Milestones

The milestones follow the proof: the coupling bound (2.1); the appendix lemmas on weak convergence (A.1, A.2); the coupling estimates (6.3) and (6.2) and the independence of Step Three; optimality of every limit point; the conditional-law lemmas (A.5, A.4); the pre-limit consistency identity of Step Four; Lemma A.3; consistency of every limit point.

Significance

Theorem 6.1 identifies the limit model of large symmetric games played with a mediator. It shows that correlation does not disappear in the limit: the flow of measures recommended by the mediator may remain random, and the limit object must record its joint law with the recommendation. Together with Theorem 7.1 it makes correlated mean field game solutions the exact counterpart of $N$-player correlated equilibria, as mean field equilibria are of Nash equilibria. The example of Section 5 of the paper exhibits a correlated solution with a non-deterministic flow that is not a mixture of deterministic-flow solutions.

The result is proved in the paper; to our knowledge no part of it, nor any correlated-equilibrium mean field result, has been formalized. The mission produces a machine-checked model of discrete-time finite-state mean field games with a mediator, and general-purpose lemmas absent from Mathlib: a mapping theorem for almost everywhere continuous maps that identifies limits of relations $Y_n=\Psi(Z_n)$, converging together on varying probability spaces, limits of regular conditional distributions, and the conditional law of an exchangeable coordinate given the empirical measure.

Difficulty

Compactness is immediate because all spaces are compact. The content is in identifying the limit. Two obvious steps fail. First, the system function is discontinuous (as in Remark 6.1), so the dynamics do not pass to the limit by the continuous mapping theorem; only almost-everywhere continuity with respect to measures of the form $\tau\otimes\nu$ is available. Second, a unilateral deviation by player 1 changes the empirical measures seen by all other players, and through them the whole flow, so it is not clear that the limit flow under a deviation is the limit flow without it. Third, conditional laws are not continuous under convergence in distribution, yet consistency, a statement about the conditional law of the state given the whole flow, must survive the limit.

Formalization scope

The Lean development lives in the namespace SimpleCorrMFG.Conv. $\mathcal P(\mathcal X)$ is stdSimplex ℝ X with its subspace topology and Borel σ-algebra; flows are Fin (T+1) → P(X); restricted strategies are Fin T → X → Γ; times of actions and noises are Fin T (the noise $\xi(t+1)$ has index $t$); players are Fin N and the paper's player 1 is index 0; $\nu$ is volume on unitInterval. Probability measures on $\mathcal R\times\mathcal P(\mathcal X)^{T+1}$ are Mathlib's ProbabilityMeasure with the topology of weak convergence, and a limit point is the limit of a subsequence with strictly increasing indices.

The paper defines costs and $\rho^N$ through "any realization" and notes that they do not depend on the choice. The formalization uses the canonical realization: the product law of initial states, recommendations (or the correlated flow) and noises, with the states computed by the recursion. The consistency condition is stated as $\mathbb P(X(t)=x,\ \mu\in B)=\mathbb E[\mathbf 1_B(\mu)\,\mu(t)(\{x\})]$ for every $t$, $x$ and Borel $B$, which is the definition of a regular conditional distribution given the whole flow. (A3) is required for $N\ge2$, where the $N$-player game is defined.

A formalization in which the flow is conditioned only up to time $t$, in which the costs are integrals of possibly non-integrable functions, or in which "limit point" refers to a topology other than weak convergence would prove a different and weaker statement and is excluded. The standing assumptions that $\Psi$ is measurable and $f,F$ are bounded and measurable are carried explicitly, so that no expected cost or law is a junk value.

Contributions are welcome on each milestone. The appendix lemmas are independent of the game and reusable. The written proof of (6.2) uses $\mathbb E[w(\mathrm{dist})]\to0$; since (A1) does not require $w(0)=0$, this step needs the observation that the indicator in (A1) vanishes when the two measures coincide.

Selected references

• L. Campi, M. Fischer, Correlated equilibria and mean field games: a simple model, arXiv:2004.06185v2, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2004.06185
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1, 67–96, 1974. https://doi.org/10.1016/0304-4068(74)90037-8
• S. Hart, D. Schmeidler, Existence of correlated equilibria, Mathematics of Operations Research 14(1), 18–25, 1989. https://doi.org/10.1287/moor.14.1.18
• J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2, 229–260, 2007. https://doi.org/10.1007/s11537-007-0657-8
• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, Annals of Applied Probability 30(4), 1693–1761, 2020. https://doi.org/10.1214/19-AAP1541
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968.
• O. Kallenberg, Foundations of Modern Probability, 2nd ed., Springer, 2001 (Lemma 11.11). https://doi.org/10.1007/978-1-4757-4015-8

Motivation

Supermarkets run temporary price promotions on a large share of their assortment, and the choice of which item to discount, by how much and in which week is a recurring planning decision for category managers. Promotions on one item change the sales of the others: a discount on one brand of coffee draws customers away from a competing brand (substitution), while a discount on shampoo can raise the sales of conditioner (complementarity). Promotions also have effects over time, because customers who stockpile during a promotion buy less afterwards.

M. C. Cohen, J. J. Kalas and G. Perakis (SSRN 3061451; Management Science, 2021, doi:10.1287/mnsc.2020.3641) formulate the multi-item promotion problem as a nonlinear integer program and approximate it by a hierarchy of linear integer programs $\mathrm{App}(\kappa)$, which add up the profit contributions of promoting up to $\kappa$ items together. Their single-item predecessor, Cohen, Leung, Panchamgam, Perakis and Smith (Operations Research, 2017), corresponds to $\mathrm{App}(1)$. The main structural result of the multi-item paper, its Theorem 1, says that under a common separability assumption on demand the hierarchy collapses at level two.

Setting

There are $N$ items and a selling season of $T$ periods. The retailer has enough inventory to meet demand throughout the season, as assumed in §2.1, so inventory does not enter the model. Item $i$ has a price ladder $q^{i0},q^{i1},\dots,q^{iK^i}$, where $q^{i0}=q^0$ is the regular price, common to all items, and the other points are promotion prices. A plan $\gamma$ chooses a level $\gamma^i_t\in\{0,\dots,K^i\}$ for every item and period; the price of item $i$ at period $t$ is $p^i_t=q^{i\gamma^i_t}$. Item $i$ has unit costs $c^i_t$ and a memory $M^i$, and its demand at period $t$ is a function

$$d^i_t\big(p^i_t,p^i_{t-1},\dots,p^i_{t-M^i},\mathbf p^{-i}_t\big)$$

of its own current and $M^i$ past prices and of the other items' current prices (Assumption 1: cross past prices do not enter). The total profit of a plan is

$$\mathrm{MPOP}(\gamma)=\sum_{i=1}^N\sum_{t=1}^T(p^i_t-c^i_t)\,d^i_t\big(p^i_t,\dots,p^i_{t-M^i},\mathbf p^{-i}_t\big),$$

and the problem (Multi-POP) maximizes it over plans satisfying the business rules: at most $L^i$ promotions of item $i$, at most one promotion of item $i$ in any $S^i+1$ consecutive periods, at most $L_T$ promotions in total and at most $C_t$ in period $t$.

A pattern $\sigma$ assigns a level $\sigma_i$ to each item; its support $S(\sigma)$ is the set of promoted items. The pure promotion vector $\mathbf p^\sigma_t$ uses $\sigma$ at period $t$ and the regular price everywhere else, and $\mathbf p^0$ is the all-regular plan. The coefficient of $\sigma$ at $t$ is the inclusion–exclusion sum

$$b^\sigma_t=\sum_{U\subseteq S(\sigma)}(-1)^{|S(\sigma)|-|U|}\,\mathrm{MPOP}\big(\mathbf p^{\sigma|_U}_t\big),$$

where $\sigma|_U$ keeps the levels of $\sigma$ on $U$ and is regular off $U$. With one promoted item this is $b^{kj}_t=\mathrm{MPOP}(\mathbf p^{kj}_t)-\mathrm{MPOP}(\mathbf p^0)$, equation (5); with two it is equation (6). The App(κ) objective of a plan is

$$\mathrm{MPOP}(\mathbf p^0)+\sum_{t=1}^T\sum_{\sigma:\,1\le|S(\sigma)|\le\kappa}b^\sigma_t\,\mathbf 1\{\gamma^i_t=\sigma_i\ \forall i\in S(\sigma)\},$$

which is equation (4) for $\kappa=2$, and $\mathrm{App}(\kappa)$ maximizes it over the same feasible set.

Formalization targets

Goal: Theorem 1

Assume the cross-item effects are additively separable,

$$d^i_t\big(p^i_t,\dots,p^i_{t-M^i},\mathbf p^{-i}_t\big)=h^i_t\big(p^i_t,\dots,p^i_{t-M^i}\big)+\sum_{j\neq i}H^{ji}_t(p^j_t),\qquad(8)$$

for arbitrary functions $h^i_t$ and $H^{ji}_t$. Then for every $2\le\kappa\le N$ and all business-rule data,

$$\mathrm{App}(\kappa)\text{ objective}=\mathrm{App}(2)\text{ objective at every plan},\qquad \operatorname{argmax}\mathrm{App}(\kappa)=\operatorname{argmax}\mathrm{App}(2).$$

This is the chain $\mathrm{App}(2)=\mathrm{App}(3)=\dots=\mathrm{App}(N)$ of the paper.

Milestones

1. The recursion before (16) (p. 38): for a nonempty support $S$, $b^\sigma_t=\mathrm{MPOP}(\mathbf p^\sigma_t)-\mathrm{MPOP}(\mathbf p^0)-\sum_{\emptyset\ne U\subsetneq S}b^{\sigma|_U}_t$, for any demand.
2. Locality (p. 37): the coefficient is the sum of item–period contributions, and under (8) with $|S|\ge2$ the contributions at periods other than $t$ and of unpromoted items are zero.
3. Order three, (15) (p. 37): under (8), every coefficient with three promoted items is zero.
4. All orders (pp. 37–39): under (8), every coefficient with at least three promoted items is zero.
5. The binary-IP remark (p. 14): if a function of binary variables is a sum of functions each depending on at most two variables, all its inclusion–exclusion coefficients of order at least three vanish.

Significance

The size of $\mathrm{App}(\kappa)$ grows like $N^\kappa$ in the number of pairwise, triple and higher variables, and $\mathrm{App}(N)$ has a variable for every subset of items. Theorem 1 shows that under (8) nothing is gained beyond $\mathrm{App}(2)$, an integer program with a quadratic number of variables. Equation (8) covers the demand models used in practice that the paper cites, the log-linear model with linear cross terms and the linear cross-elasticities model. The rest of the paper's solution approach works with $\mathrm{App}(2)$: integrality of its LP relaxation for substitutable items (Theorem 2), a rounding scheme and a parametric bound (§3); Theorem 1 is what makes $\mathrm{App}(2)$ the complete cross-item model under (8).

The result is proved in the paper; its appendix carries out the order-three case explicitly and the induction step in outline, with "the details … omitted for conciseness". No machine-checked proof is known to exist. A formal proof removes the omitted cancellations and isolates the combinatorial core (milestone 5), which is a fact about pseudo-Boolean functions useful beyond promotions.

Difficulty

The coefficients are signed sums of $2^{|S|}$ total profits over all $N$ items and $T$ periods, and each profit is a product of a price margin and a demand that depends on a window of past prices. The obvious idea, expanding the products directly, gives an unmanageable number of terms. Every contribution involving three or more promoted items has to cancel, including the contributions at later periods, which see a promotion only through the memory window, and the paper omits these cancellations in the general induction step. Without (8) the claim fails: the paper notes that for demand models violating it $\mathrm{App}(2)$ is not necessarily equal to $\mathrm{App}(N)$, and a demand with a three-way cross term already has nonzero order-three coefficients.

Formalization scope

Lean namespace PromoMulti.PairwiseExact. Items are Fin N and periods Fin T, 0-based (period $t$ of the paper is index $t-1$); prices, costs and profits are real. A plan is a function assigning a level Fin (K i + 1) to each item and period, level 0 being the regular price $q^0$; this is the binary encoding $\gamma^{ik}_t$ with $\sum_k\gamma^{ik}_t=1$. Prices before the first period are $q^0$ (the appendix evaluates $h^i_t(p^i_t,q^0,\dots,q^0)$); Theorem 1 holds for any fixed history. The paper's pairwise variables $\gamma^{k\ell ij}_t$ are separate binaries tied by the consistency constraints (7); for integral plans (7) forces them to be products, and the App(κ) objective uses that product directly. The paper writes $\mathrm{App}(\kappa)$ out only for $\kappa\le2$; for $\kappa\ge3$ the formalization uses the inclusion–exclusion extension of (4) with the general coefficient of p. 38. The demand receives the whole current price vector; (8) reads only the coordinates $j\ne i$. The ladder order $q^{iK^i}<\dots<q^{i1}<q^0$ is not imposed, nor any monotonicity, linearity or sign of $h$ and $H$: Theorem 1 uses none. The business rules are those of (Multi-POP); the inter-item rules 2, 3 and 5 of §2.2 are not part of it.

The coefficients are defined by the closed alternating sum and the App(κ) objective sums every pattern with $1\le|S|\le\kappa$; a formalization that defines App(κ) through pairs only, defines higher coefficients as zero, or defines coefficients by the recursion (16) makes the goal trivial and is ruled out. The goal does not claim that App(2) solves (Multi-POP), which is false when past prices matter.

A complete development needs finite inclusion–exclusion over Finset.powerset, the cancellation lemma of milestone 5 (reusable for any pseudo-Boolean or multi-level function that is a sum of low-arity terms), and the bookkeeping of which plan coordinates each item–period profit reads. Contributions of proofs of any milestone, of milestone 5 in greater generality, and of alternative arguments are welcome.

Selected references

• M. C. Cohen, J. J. Kalas, G. Perakis, Promotion Optimization for Multiple Items in Supermarkets, Management Science, 2021; preprint SSRN 3061451. https://ssrn.com/abstract=3061451, https://doi.org/10.1287/mnsc.2020.3641
• M. C. Cohen, N.-H. Z. Leung, K. Panchamgam, G. Perakis, A. Smith, The Impact of Linear Optimization on Promotion Planning, Operations Research 65(2), 2017. https://doi.org/10.1287/opre.2016.1573

Motivation

A discrete moment problem asks for the largest expected payoff compatible with prescribed moments of an unknown probability distribution. A decision maker may know the first few moments of demand or loss while the full distribution remains uncertain. The optimization then asks which compatible distribution makes a chosen payoff largest. Chen, He, Jiang, Ryan, and Zhang study what happens when the distribution must also obey a shape constraint. Their preprint treats discrete log-concavity and increasing failure rate as two such constraints. This mission concerns the log-concave case.

The moment constraints alone define a convex polytope of probability vectors. Requiring log-concavity changes its geometry: the feasible region is generally nonconvex. This matters because familiar descriptions of extreme points of a moment polytope no longer describe the candidate worst-case distributions. The paper's Theorem 4.1 gives a finite structural description of the optimal extreme points despite that change. Its proof uses a general result about optimization over reverse convex constraints, Theorem 3.6, which is also included as a milestone. Both statements and their setting are taken from arXiv:1708.02079v1, pages 5–15.

Setting

Fix the finite sample space $\Omega=\{1,\ldots,n\}$. A distribution is a vector $x=(x_1,\ldots,x_n)$ of nonnegative masses. For each integer $i$ from $0$ through $m$, its prescribed moment is $q_i$, so $\sum_{j=1}^{n}j^i x_j=q_i$. The convention $q_0=1$ makes the masses sum to one. Given payoff coefficients $f_j$, the discrete moment problem maximizes $\sum_{j=1}^{n}f_jx_j$ over the distributions satisfying these equations.

A distribution is discrete log-concave when its positive masses form one consecutive integer interval $[k,\ell]$ and $x_{j-1}x_{j+1}\le x_j^2$ at every interior index $k<j<\ell$. In the paper's formulation (DMP-LC), the entries on $[k,\ell]$ are strictly positive and the other entries are zero; the feasible region is the union over all such supports. Its alternative formulation (DMP-LC′) replaces the chosen support with nonnegativity and a family of longer-range inequalities. Proposition 2.4 says that the two feasible regions coincide. The extreme points in this mission are those of the entire feasible region, including every possible support.

The paper also considers a general reverse convex program in $\mathbb R^n$: minimize a function $c(x)$ subject to $Ax=b$, $x\ge0$, and $f_p(x)\le0$ for $p=1,\ldots,P$. Here the reverse convex condition is relative to the nonnegative orthant: the forbidden set $\{x\ge0:f_p(x)>0\}$ is convex. Under the paper's continuity, quasiconcavity, differentiability, rank, and compactness assumptions, Theorem 3.6 counts the inequalities that are tight at an optimal extreme point.

Formalization targets

The goal is the corrected mathematical content of Theorem 4.1. If (DMP-LC) is feasible, an optimal extreme point exists. Every optimal extreme point $x^*$ has support $[k,\ell]$ and can be covered by at most $m$ geometric pieces. In symbols, there are weakly increasing breakpoints $k=b_0\le b_1\le\cdots\le b_m=\ell$ and positive parameters $\alpha_i,r_i$ such that

$$x_j^*=\alpha_i r_i^{j-b_{i-1}}\quad\text{for }b_{i-1}\le j\le b_i, \qquad x_j^*=0\quad\text{outside }[k,\ell].$$

The milestone path includes the equivalence of the two feasible formulations, compact-set extreme-point results, convexity of the forbidden power regions, the reverse convex tight-constraint count, and the two structural steps in the proof of Theorem 4.1. Theorem 3.6 asserts, in particular, that at each optimal extreme point of its $m$-row program,

$$n-m\le \#\{p:f_p(x^*)=0\}+\#\{j:x_j^*=0\}.$$

Significance

The conclusion replaces an unrestricted search over feasible probability vectors with a characterization of the candidates that can be optimal extreme points. It also identifies how the number of prescribed nonzero-order moments controls the number of geometric pieces. The count in Theorem 3.6 applies to the larger class of reverse convex programs described above; it is useful independently of this distributional example. These are results proved in the cited preprint, rather than open conjectures.

The formalization target is to give the known statements a machine-checked proof in Lean. The proposed items are statements with proof placeholders; they do not yet assert that a machine-checked proof exists. The finite moment notation, the log-concave feasible region, and the reverse convex feasible region are separate definition files so the general finite-dimensional objects can be reused. Contributions to the milestone theorems, the proof of the goal, and supporting lemmas are all in scope.

Difficulty

The log-concavity inequalities do not make the feasible region convex, so the standard convex-polytope description of optimal extreme points does not directly apply. In addition, the chosen support may move: a vector that is extreme within one fixed-support slice need not be extreme in the full union. Existence of an optimal solution alone gives no bound on the number of geometric pieces. The challenge is to obtain enough tight constraints at every optimal extreme point, then relate those equalities to its coordinates without assuming the desired shape in the definition of feasibility.

Formalization scope

Lean represents $\mathbb R^n$ as Fin n → ℝ; a Fin n index with value $j-1$ represents the paper's position $j$. The helper ext supplies the paper's one-based coordinates and returns zero outside $[1,n]$. Moments use the exact weights $w_j=j$. All feasible sets use real vectors, with nonnegativity or strict positivity stated where the paper requires it. The (DMP-LC) region is the union over supports satisfying (2b)–(2e); the goal uses extreme points of that whole set and a maximization objective. The reverse convex milestones use minimization, full row rank, and convexity of the forbidden sets inside the nonnegative orthant. Compactness and nonemptiness are explicit assumptions where the source invokes them.

Two corrections to the printed Theorem 4.1 are necessary. First, its bound $0<r_i<1$ is false. With $n=3$, $m=1$, $q_0=1$, $q_1=5/2$, and payoff $f=(1,0,0)$, the unique maximizing extreme point is approximately $(0.1162,0.2676,0.6162)$, whose geometric ratio is about $2.30$. The formal statement requires $r_i>0$. Second, the printed strict chain of breakpoints fails for short supports: with $n=3$, $m=2$, and moments $(q_0,q_1,q_2)=(1,2,4)$, the only feasible distribution is the point mass at $2$. Weak breakpoints express the paper's “at most $m$ pieces” conclusion. They allow degenerate pieces; $m=0$ is retained and forces a point mass. The proof's closed-range wording for tight equalities is read on interior indices, and the tight count uses $m+1$ moment rows. These choices and the paper's typographical slips are recorded with the items.

The feasible region does not encode geometric sequences, and extremeness is never taken only within one support or within its convex hull. The development needs Mathlib's finite sums, finite-dimensional topology, convex hulls, extreme points, matrix rank, continuity, quasiconcavity, and differentiation. The finite discrete moment definition and reverse convex feasible-set definition are intended for reuse beyond this paper.

Selected references

• X. Chen, S. He, B. Jiang, C. T. Ryan, and T. Zhang, The Discrete Moment Problem with Nonconvex Shape Constraints, preprint arXiv:1708.02079v1, 2017; published in Operations Research, 2021. Pinned preprint.

Motivation

A minimum support price (MSP) guarantees farmers a unit sale price at least as high as an announced floor. It can protect farmers when the market price is low, but the same guarantee can require a government payment and can change how much crop is produced. Policy evaluation therefore needs to account for farmers, consumers, and public expenditure together. Chintapalli and Tang examine these effects when the market price is uncertain and farmers decide whether to sow before that price is known (SSRN manuscript, §§3–4). This mission takes the paper's market uncertainty model and its joint assessment of farmer net benefit and net social value. The result is already proved in the paper; the work here is to formalize its definitions and claims in Lean.

Setting

The farmer population has total mass one. Each farmer can produce one unit and has a cultivation cost $c$ uniformly distributed on $[0,1]$. A farmer is small enough to take the eventual market price as given. At total production $q$, the inverse demand price is $p(q,\epsilon)=a-q+\epsilon$, where $a$ is market potential and the shock $\epsilon$ is uniform on $[-\theta,\theta]$. The government announces an MSP $m$ before sowing. A participating farmer receives the effective price $\hat p(m,q,\epsilon)=\max\{m,p(q,\epsilon)\}$: the market price when it exceeds the guarantee and the guaranteed price otherwise (manuscript, pp. 6–8).

Farmers are risk averse according to the paper's value-at-risk participation rule. A farmer with cost $c$ finds the crop lucrative when the probability that effective price is no greater than cost is at most $\alpha$:

$$\Pr\{\hat p(m,q,\epsilon)\le c\}\le\alpha.$$

The equilibrium quantity $q(m)$ equals the mass of farmers whose costs make cultivation lucrative when aggregate production is $q(m)$. The model does not prescribe this quantity in advance. Write $\tau_0=(a-(1-2\alpha)\theta)/2$ for production without an effective guarantee and $\tau(m)=\min\{1,\max\{m,\tau_0\}\}$ for the quantity identified by Theorem 1. The paper considers admissible MSPs $m\in\mathcal M$: the guarantee lies between the lowest and highest possible market price at its equilibrium quantity, or $a-q(m)-\theta\le m\le a-q(m)+\theta$ (manuscript, eqs. (7) and (9), pp. 8–10).

Let $F(m)$ be aggregate expected farmer surplus, computed from the effective sale price less each participating farmer's cost. Let $E(m)$ be government expenditure on the positive difference between the guarantee and the market price. Let $C(m)$ be consumer surplus, the area between inverse demand and the market price over units consumed. The paper evaluates a guarantee through net benefit $B(m)=F(m)-E(m)$ and net social value $V(m)=F(m)+C(m)-E(m)$ (manuscript, pp. 7 and 11–12).

Formalization targets

The milestone path first identifies individual participation and the unique equilibrium quantity, then establishes the paper's explicit formulas for $F$, $E$, and $C$. Two identities in the proof of Proposition 1 summarize the resulting policy values for admissible $m$:

$$B(m)=\tau(m)\left(a-\frac32\tau(m)\right),\qquad V(m)=\tau(m)\bigl(a-\tau(m)\bigr).$$

The goal is Proposition 1 in full. When $a\le3/2$ and $\tau_0\le m\le1$, it states $B(m)\ge0$ if and only if $m\le2a/3$. It identifies an admissible maximizer of net benefit at $m_B=\max\{\tau_0,\min\{1,a/3\}\}$ and says net benefit is independent of $m$ in each of the regions $m\le\tau_0$ and $m\ge1$. It also states $V(m)>0$ for every admissible $m$ and identifies an admissible maximizer at $m_V=\min\{1,a/2\}$ (manuscript, Proposition 1, p. 13). A maximizer is a price attaining the largest value; the proposition does not require uniqueness.

Significance

The two metrics answer different policy questions. Net benefit asks whether farmers' aggregate surplus exceeds the public cost of the support guarantee. Net social value adds consumer surplus to that accounting. Proposition 1 identifies which MSP maximizes each measure and states that the broader value remains positive throughout the admissible range. These conclusions are specific to the paper's linear inverse demand, continuous uniform cost and price shock, and risk-based sowing rule; they do not claim the same price choices for other agricultural markets (manuscript, §4.3).

Formalizing the result requires a machine-checkable account of the continuum of farmer costs, the uniformly distributed market shock, a fixed-point equilibrium, and integrals defining all three welfare components. The manuscript gives a proof; the Lean theorem files in this proposal state open proof obligations. A completed development would make the integral formulas, equilibrium characterization, and optimality claims reusable for related support-price models, while exposing exactly which modeling assumptions they need.

Difficulty

The farmer's sowing decision depends on the distribution of the effective price, and the effective price changes at the support threshold. At the same time, the market price depends on the aggregate number of farmers who sow. Directly inserting a guessed production quantity would skip the equilibrium question. The welfare formulas add a second layer: they must integrate the same participation rule and price guarantee, then compare policies only within the admissible set. Theorem 1's printed farmer-level biconditional also has a boundary cost that requires care, even though a single cost has zero mass under the uniform distribution (manuscript, Theorem 1 and its proof, pp. 10 and 37).

Formalization scope

Lean represents prices, costs, probabilities, and welfare values in $\mathbb R$. The cost distribution is Lebesgue measure on $[0,1]$; the shock law is normalized Lebesgue measure on $[-\theta,\theta]$. The standing assumptions are $0<\alpha<1/2$, $\theta>0$, $1+\theta<a$, and $\tau_0<1$. Positivity of $\theta$ is explicit in Lean because the uniform law and its expectation divide by $2\theta$. The paper treats it implicitly when it specifies a nondegenerate uniform shock. The lucrative rule uses weak inequalities on both the loss event and the probability bound, following the numbered model equations (manuscript, eqs. (1), (5), and (6)).

An MSP's admissibility is evaluated at an equilibrium quantity, not at an arbitrary guessed quantity. Equilibrium is defined as a fixed point of the mass of lucrative farmers; it is not defined to equal $\tau(m)$. Farmer surplus, expenditure, and consumer surplus are integrals, not the later closed forms. This prevents the goal from becoming a substitution exercise. Theorem 1 is restricted to admissible MSP values; its premise evaluates admissibility at the proposed equilibrium $\tau(m)$, which the theorem then identifies as the actual equilibrium. Its farmer-level clause excludes the one threshold cost at which the manuscript's biconditional is inaccurate. Aggregate equilibrium remains the same. The mission covers the single-crop market uncertainty model in §§3–4; the paper's yield uncertainty and two-crop extensions are separate results. Contributions to the fixed-point, measure, integration, and policy-optimization steps are all within scope.

Selected references

• P. Chintapalli and C. S. Tang, The Value and Cost of Crop Minimum Support Price: Farmer and Consumer Welfare and Implementation Cost, Management Science 67 (2021), doi:10.1287/mnsc.2020.3831. The formalized statements and page numbers follow the authors' SSRN manuscript 3681588.

Motivation

Temporal-difference (TD) learning is the basic algorithm of reinforcement learning for estimating the value function of a fixed policy from a single stream of experience. With a linear function approximation $V_\theta(s)=\phi(s)^\top\theta$, TD(0) is the evaluation step inside many policy-iteration and actor–critic methods, and its behaviour governs how much data such methods need.

The asymptotic theory is classical. Tsitsiklis and Van Roy (1997) proved that TD(λ) with linear features converges almost surely along a single trajectory of an ergodic Markov chain, to the unique solution $\theta^*$ of the projected Bellman equation, under Robbins–Monro step sizes. Their proof uses the ODE method, which says nothing about how fast the iterates approach $\theta^*$, nor how the rate depends on the step size, on the conditioning of the features, or on how quickly the chain mixes.

Finite-time results came later and mostly for independent samples. Dalal, Szörényi, Thoppe and Mannor (2018) and Lakshminarayanan and Szepesvári (2018) analysed TD(0) when the observed transitions are drawn i.i.d. from the stationary distribution. Bhandari, Russo and Singal (2018) gave a short analysis in the i.i.d. model and, for a projected variant of TD, the first finite-time bounds when the transitions come from one trajectory of the Markov chain, so that consecutive observations are strongly correlated. This mission formalizes that Markovian result, Theorem 3 of the paper.

Setting

A finite Markov reward process consists of a finite state space $S$, a stochastic matrix $P$ with $P(s,s')$ the probability of moving from $s$ to $s'$, transition rewards $R(s,s')$ with $|R(s,s')|\le r_{\max}$, and a discount factor $0\le\gamma<1$. The chain has a stationary distribution $\pi$ ($\pi P=\pi$), and the observed trajectory $s_0,s_1,\dots$ starts from $\pi$, so it is a stationary sequence.

Each state carries a feature vector $\phi(s)\in\mathbb{R}^d$ with $\|\phi(s)\|_2\le1$. The steady-state feature covariance $\Sigma=\sum_s\pi(s)\phi(s)\phi(s)^\top$ has full rank, and $\omega>0$ is its minimum eigenvalue. Value functions are compared in the steady-state seminorm $\|V_\theta\|_D^2=\sum_s\pi(s)(\phi(s)^\top\theta)^2$.

At a transition $(s,s')$ the TD direction is $g(\theta;s,s')=\big(R(s,s')+\gamma\phi(s')^\top\theta-\phi(s)^\top\theta\big)\phi(s)$. Its steady-state mean is $\bar g(\theta)=\sum_{s,s'}\pi(s)P(s,s')\,g(\theta;s,s')$, and the TD fixed point $\theta^*$ is the vector with $\bar g(\theta^*)=0$. Projected TD(0) with radius $R\ge\|\theta^*\|_2$ starts from $\|\theta_0\|_2\le R$ and iterates

$$\theta_{t+1}=\Pi_{2,R}\big(\theta_t+\alpha_t\,g(\theta_t;s_t,s_{t+1})\big),$$

where $\Pi_{2,R}$ is the Euclidean projection onto the ball of radius $R$. The averaged iterate is $\bar\theta_T=T^{-1}\sum_{t=0}^{T-1}\theta_t$.

The chain mixes uniformly (Assumption 1): there are $m>0$ and $\rho\in(0,1)$ with $\sup_s d_{TV}(P^t(s,\cdot),\pi)\le m\rho^t$ for all $t\ge0$. The mixing time is $\tau_{\mathrm{mix}}(\epsilon)=\min\{t\ge0: m\rho^t\le\epsilon\}$. Write $G=r_{\max}+2R$.

Formalization targets

Goal: Theorem 3 (pp. 17–18)

All three bounds are stated together, with $\mathbb{E}$ the expectation over the stationary trajectory:

(a) for $T\ge1$ and $\alpha_t\equiv1/\sqrt T$,

$$\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{\|\theta^*-\theta_0\|_2^2+G^2\big(9+12\tau_{\mathrm{mix}}(1/\sqrt T)\big)}{2\sqrt T(1-\gamma)};$$

(b) for a constant $\alpha_t\equiv\alpha_0\in\big(0,\,1/(2\omega(1-\gamma))\big)$,

$$\mathbb{E}\|\theta^*-\theta_T\|_2^2\le e^{-2\alpha_0(1-\gamma)\omega T}\|\theta^*-\theta_0\|_2^2+\alpha_0\frac{G^2\big(9+12\tau_{\mathrm{mix}}(\alpha_0)\big)}{2(1-\gamma)\omega};$$

(c) for $\alpha_t=1/(\omega(t+1)(1-\gamma))$ and $T\ge1$,

$$\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{G^2\big(9+24\tau_{\mathrm{mix}}(\alpha_T)\big)}{T(1-\gamma)^2\omega}(1+\log T).$$

Milestones

The milestones are the paper's own lemmas, in the order the proof in Appendix A uses them: norm equivalence $\sqrt\omega\|\theta\|_2\le\|V_\theta\|_D\le\|\theta\|_2$ (Lemma 1); the descent inequality $(\theta^*-\theta)^\top\bar g(\theta)\ge(1-\gamma)\|V_{\theta^*}-V_\theta\|_D^2$ (Lemma 3); the gradient bound $\|g_t(\theta)\|_2\le r_{\max}+2\|\theta\|_2$ (Lemma 6); the pathwise error recursion (Lemma 8); the coupling bound $|\mathbb{E}v(X,Y)-\mathbb{E}v(X',Y')|\le2\|v\|_\infty m\rho^\tau$ (Lemma 9); boundedness and Lipschitz continuity of the gradient error $\zeta_t$ (Lemma 10); and the bias bound $\mathbb{E}[\zeta_t(\theta_t)]\le G^2(4+6\tau_{\mathrm{mix}}(\alpha_T))\alpha_{t^*}$ (Lemma 11).

Significance

Theorem 3 gives explicit, non-asymptotic mean-squared-error bounds for TD(0) with linear features under Markovian sampling. Part (a) does not depend on the conditioning $\omega$, part (b) shows exponential convergence to a neighbourhood whose radius scales with $\alpha_0G^2\tau_{\mathrm{mix}}(\alpha_0)$, and part (c) gives an $\tilde O(1/T)$ rate. Compared with the i.i.d. bounds, the only change is a factor of order $\tau_{\mathrm{mix}}$: roughly, one mixing time of correlated observations is worth one independent sample. The same argument carries over, in the paper itself, to projected TD(λ) (Theorem 4) and to Q-learning for optimal stopping (§10), so the lemmas formalized here are the core of all of its Markovian results.

The result is proved on paper but has not been machine-checked. The mission provides a Lean statement of the theorem and of each lemma of its proof, all built on one model. The trajectory-level definitions (path law, total-variation mixing, mixing time, projected iterates) can be reused by later formalizations of Markovian stochastic approximation.

Difficulty

The obvious approach, from the i.i.d. analysis, takes expectations in the error recursion of Lemma 8 and uses $\mathbb{E}[\zeta_t(\theta_t)]=0$. Under Markov sampling this fails: $\theta_t$ is a function of $s_0,\dots,s_t$ and is correlated with the observation $(s_t,s_{t+1})$ at which it is evaluated, so the gradient is biased and the noise is not a martingale difference. Bounding that bias needs a quantitative decorrelation between the iterate $\tau$ steps back and the current observation, which is a total-variation estimate on the joint law of a path (Lemma 9). It also needs control of how far the iterates drift in $\tau$ steps, which is where the projection and the uniform gradient bound $G$ enter. The rest of the proof then combines telescoping, a geometric recursion and harmonic sums, with every constant ($9+12\tau$, $9+24\tau$) tracked exactly.

Formalization scope

• State space and expectation. $S$ is a Fintype. The expectation over the stationary trajectory is the finite sum $\sum_{w\in S^{T+1}}\pi(w_0)\prod_iP(w_i,w_{i+1})\,F(w)$, the exact law of $(s_0,\dots,s_T)$ for a finite chain started from $\pi$, so no measure theory is used. The paper itself works with a finite $S$ (p. 5).
• Coupling lemma. Lemma 9 uses probability measures for the conditional laws of $X,Y$ given $s_t,s_{t+\tau}$; their factorization expresses $X\to s_t\to s_{t+\tau}\to Y$. The variables may take values in arbitrary measurable spaces, including the iterates and observations used in the proof.
• Norms. Parameters and features live in EuclideanSpace ℝ (Fin d) with $d\ge1$, so every $\|\cdot\|$ is Euclidean.
• Standing hypotheses, added or made explicit: $0\le\gamma$ (the paper writes $\gamma<1$; the proof of Lemma 3 needs $\gamma\ge0$). $\omega$ is the least value of $\theta^\top\Sigma\theta$ on the unit sphere, that is $\lambda_{\min}(\Sigma)$, together with $\omega>0$ (full rank). $\pi$ is a stationary probability vector, and no separate irreducibility hypothesis is added, since Assumption 1 implies ergodicity. $\theta^*$ is given as a vector with $\bar g(\theta^*)=0$. The implicit conditions are explicit: $T\ge1$ in (a) and (c), $\alpha_0>0$ in (b), $\alpha_T>0$ in Lemma 11, and $\alpha_t\ge0$ in Lemma 8.
• Conventions. $\Pi_{2,R}$ is defined by the rescaling formula of p. 16. $\bar\theta_T$ averages $\theta_0,\dots,\theta_{T-1}$, as in the text and the proof (Algorithm 1's averaging recursion is a slip). $\tau_{\mathrm{mix}}$ is sInf over $\mathbb{N}$ and is only evaluated at positive thresholds, where it is a true minimum. "With probability 1" is stated for every path or transition.
• No trivialization. The expectation must start from $\pi$, never from an arbitrary state. $\theta_t$ and the observation must come from the same trajectory. $\omega$ must be $\lambda_{\min}(\Sigma)$, not an arbitrary positive constant, since it fixes the step size in (c). A formalization with independent samples, with the sup norm on $\mathbb{R}^d$, or with a junk-valued $\tau_{\mathrm{mix}}(0)=0$ would prove a different statement.
• Not in scope. Theorem 1 (mean-path TD), Theorem 2 (i.i.d. model), Theorem 4 (projected TD(λ)) and §10 (Q-learning for optimal stopping) are separate results. Theorem 3's proof does not use them.
• Welcome contributions. Proofs of the milestones, and general lemmas on finite path sums (marginalisation of the trajectory law, the variational form of total variation, nonexpansiveness of the ball projection).

Selected references

• J. Bhandari, D. Russo, R. Singal, A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximation, arXiv:1806.02450v2, 2018; Operations Research 69(3), 2021. https://arxiv.org/abs/1806.02450
• J. N. Tsitsiklis, B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
• G. Dalal, B. Szörényi, G. Thoppe, S. Mannor, Finite Sample Analyses for TD(0) with Function Approximation, AAAI 2018. https://arxiv.org/abs/1704.01161
• C. Lakshminarayanan, C. Szepesvári, Linear Stochastic Approximation: How Far Does Constant Step-Size and Iterate Averaging Go?, AISTATS 2018. http://proceedings.mlr.press/v84/lakshminarayanan18a.html
• R. S. Sutton, Learning to Predict by the Methods of Temporal Differences, Machine Learning 3, 1988. https://doi.org/10.1007/BF00115009
• D. A. Levin, Y. Peres, Markov Chains and Mixing Times, 2nd ed., AMS, 2017. https://doi.org/10.1090/mbk/107

Motivation

Electricity end-users increasingly generate their own power with rooftop solar panels and small wind turbines. This distributed renewable energy (DRE) is usually sold under net metering: a customer who produces less than it consumes buys the shortfall from its utility at the retail price, and a customer who produces more sells the surplus back to the utility. The buy-back rate is either the retail price (the retail-based rule) or the wholesale price (the market-based rule); both are in force in different U.S. states.

The common view in the industry is that net-metered DRE hurts utilities twice: it shrinks their retail sales, and it obliges them to buy surplus energy at a rate above their procurement cost. Utilities have lobbied against net metering on this basis. Sunar and Swaminathan (SSRN 3257925; Management Science, 2021, doi:10.1287/mnsc.2020.3854) point out that this view ignores the wholesale market. A utility that meets part of its demand from a wholesale market, where generators compete in supply functions as in Klemperer and Meyer (1989) and Green and Newbery (1992), pays a market-clearing price that falls when DRE lowers the net wholesale demand. Their main result, Theorem 1, gives an exact condition under which net-metered DRE raises a utility's expected profit.

Setting

Wholesale market. There are $N > 2$ generators. Generator $n$ submits a supply function $S_n : \mathbb R \to \mathbb R$ and producing $q$ costs it $cq^2$, with $c > 0$. For a realized net wholesale demand $\mathcal D_w$, the market-clearing price $p^*_w$ solves $\sum_n S_n(p^*_w) = \mathcal D_w$. A profile is a supply function equilibrium (SFE, Definition 1) if no generator can raise its ex-post profit, for any realization of the demand, by submitting a different supply function. The symmetric profile $S_n = S$ with

$$S(p) = \frac{(N-2)\,p}{(N-1)\,2c}$$

is the equilibrium the paper works in; its clearing price is $p^*_w(\mathcal D_w) = \alpha\,\mathcal D_w$ with $\alpha = 2c(N-1)/((N-2)N)$.

Utilities. Utility $i$ sells at the retail price $p_{u,i}$. Its net-metered customers demand $D_i$ and generate $\Delta_i$; its total end-customer demand is $\widehat D_i = \beta D_i$ with $\beta > 1$. It owns existing resources covering up to $K_i \ge 0$ units at unit cost $\tilde c > 0$, with $p_{u,i} > \tilde c$. $D_i$ and $\Delta_i$ are bounded random variables, $\xi$ is the rest of the wholesale demand, and the net wholesale demand is

$$\mathcal D_w = \sum_i (\widehat D_i - K_i - \Delta_i) + \xi .$$

Utility $j$'s expected profit $\Pi_j(\ell)$ under the rule $\ell \in \{r, m\}$ is equation (6): retail revenue, minus the buy-back cost of the surplus $(\Delta_j - D_j)^+$ at $p_\ell$, minus the cost of buying the residual demand on the wholesale market, plus the revenue from selling any excess there. $\Pi_j(0)$ is the same profit when nobody generates ($\Delta \equiv 0$ everywhere, Definition 2). The constants $\nu$, $\widehat\nu$ are the expected net demands of the rest of the market with and without DRE, and $\gamma_r$, $\gamma_m$ are the explicit ratios (EC.16), (EC.17).

Formalization targets

Goal: Theorem 1 (p. 12)

For $\ell \in \{r, m\}$ there is a threshold $\bar K_\ell$ such that for every $K_j \ge 0$,

$$\Pi_j(\ell) > \Pi_j(0) \iff K_j < \bar K_\ell \ \text{ and } \ \gamma_\ell < p^{*\prime}_w(\mathcal D_w),$$

with $\gamma_\ell$ the expression (EC.16)/(EC.17), which does not depend on $K_j$.

Milestones

1. Proposition 1(a), existence: the symmetric profile $S$ is an SFE.
2. Proposition 1(a), second sentence: the clearing price is unique and equals $\alpha\mathcal D_w$, so $p^{*\prime}_w = \alpha$.
3. (EC.10), (EC.12): closed forms of $\Pi_j(r)$ and $\Pi_j(0)$.
4. (EC.11): closed form of $\Pi_j(m)$.
5. Lemma EC.1 (= Corollary 2): when $K_j = 0$, $\Pi_j(\ell) > \Pi_j(0)$ iff $\gamma_\ell < p^{*\prime}_w(\mathcal D_w)$.
6. Corollary 1 (= Lemma EC.3): $\partial(\Pi_j(\ell) - \Pi_j(0))/\partial K_j < 0$, with the printed slope.

Significance

Theorem 1 is the paper's headline: it reverses the industry's belief under stated conditions. It says that a market-reliant utility (small $K_j$) facing a wholesale price that is sensitive to demand (large $p^{*\prime}_w$) earns strictly more with net-metered DRE than without it, and that this happens only under these two conditions. Corollary 1 adds that the gain from DRE is larger the more the utility relies on the market. The paper uses these results to argue that lobbying against net metering can hurt the lobbying utility.

The result has been published but not machine-checked. A formalization pins down exactly what Theorem 1 needs, and the planning analysis already found that the printed argument leaves gaps. Lemma EC.1 is false when the denominator of $\gamma_\ell$ is not positive; a two-point counterexample is recorded in the item notes. The proof also uses an independence of region $j$ from the rest of the market that the paper does not state. Theorem 1 itself survives both gaps because its threshold $\bar K_\ell$ is existential. A Lean proof would settle this, and would also give a reusable formal account of a supply function equilibrium with quadratic costs.

Difficulty

The obvious argument says that DRE lowers retail revenue and raises buy-back costs, so the utility must lose. It fails because the wholesale price is endogenous: DRE lowers $\mathcal D_w$ and hence $p^*_w$, which helps a utility that buys on the market and hurts one that sells. Three steps carry the weight. The first is a measure-theoretic reduction of (6), with its indicator terms, to closed forms; it needs the independence of region $j$ and the integrability of every term. The second is the sign analysis of a difference that is affine in $K_j$, including the degenerate cases where $\gamma_\ell$'s denominator is $\le 0$ or the slope vanishes. The third is the ex-post optimality of the symmetric supply function against every deviation $S' : \mathbb R \to \mathbb R$, not only against differentiable or monotone ones.

Formalization scope

Everything lives in the namespace NetMeterDRE.Profit. Two definition files: SFE (profit (EC.2), clearing (1), Definition 1, $S$, $\alpha$) and Model (utility data, standing assumptions, (5), the integrand of (6), $\Pi_j(\ell)$, $\Pi_j(0)$, $\nu$, $\widehat\nu$, $\gamma_r$, $\gamma_m$). All quantities are real. Utilities are indexed by a finite type and generators by Fin N. Random primitives are measurable functions on a probability space and are almost surely bounded, so every expectation is of an integrable function. $(x)^+$ is $\max(x,0)$. The wholesale price in every theorem is a function $p_w$ that clears the market of the symmetric profile at every demand; it is neither a free differentiable function nor a closed form.

Conventions committed to:

• Added hypotheses. $(D_j, \Delta_j)$ is independent of $((D_i,\Delta_i)_{i\ne j}, \xi)$ (all items using expectations). The denominator of $\gamma_\ell$ is positive (Lemma EC.1 only). $\mathbb E[\Delta_j] > 0$ or $\nu < \widehat\nu$ (Corollary 1 only).
• Dropped, giving stronger statements. Condition (4)(b), condition (7), and the differentiability of distribution functions are not assumed.
• Not formalized. The uniqueness half of Proposition 1(a), Proposition 1(b), Lemma EC.2 (false in general), Theorems 2–3 and the §5 extensions.

The goal cannot be trivialized by the formalization. $\gamma_\ell$ is pinned to its explicit formula rather than existential, $\bar K_\ell$ is chosen before $K_j$, and $\Pi_j$ is defined by (6), not by the closed forms, so milestones 3–4 are not definitional. Contributions are welcome on any milestone. Milestones 1–2 are self-contained algebra and analysis. Milestones 3–4 are the measure-theoretic core.

Selected references

• N. Sunar and J. M. Swaminathan, Net-metered distributed renewable energy: A peril for utilities?, SSRN 3257925, version of September 2019; published in Management Science, 2021. https://ssrn.com/abstract=3257925, https://doi.org/10.1287/mnsc.2020.3854
• P. D. Klemperer and M. A. Meyer, Supply function equilibria in oligopoly under uncertainty, Econometrica 57(6), 1989. https://doi.org/10.2307/1913707
• R. J. Green and D. M. Newbery, Competition in the British electricity spot market, Journal of Political Economy 100(5), 1992. https://doi.org/10.1086/261855

Why reward design depends on entry

An innovation contest asks people outside a firm to submit solutions and promises payments according to the rank of their submissions. The firm would like a strong best submission, but a potential solver must decide whether entering is worth a fixed cost before knowing who else will enter. Paying only the winner can encourage effort while leaving the contest with no entries. Paying several ranks can make entry more attractive while spreading the reward budget across more people. Stouras, Hutchison-Krupat and Chao study that tradeoff in a model where the firm values the best solution and pays a penalty if the contest receives none (accepted SSRN version, Sections 3–5.1).

The question is operational: given a budget and entry cost, how many ranks should receive a positive reward? The paper's Theorem 2 describes regimes in which a winner-take-all allocation is optimal and regimes in which the optimum pays several ranks. Its supporting results connect the equilibrium entry threshold to the number of entrants and identify allocations that maximize participation (Theorems 1–2, pp. 10–12).

Contest and ability model

There are $n$ potential solvers, with $n\ge2$. Their abilities $A_i$ are independent draws from a common distribution on $[0,1]$ with CDF $F$ and continuous, strictly positive density $f$. A solver who exerts effort $e\ge0$ produces performance $x=ae$ when their ability is $a$. The marginal cost of effort is one. Entry also costs $c_p$, so performance $x$ costs $x/a+c_p$ for a solver with $a>0$ (model setup, pp. 6–7).

An allocation $r$ lists rank rewards $r_1\ge\cdots\ge r_n\ge0$ with $\sum_{j=1}^n r_j\le B$, where $B$ is the firm's budget. Rank one is the best submission. A rank beyond the number of entrants receives no payment. The number $m(r)$ of rewards is the count of strictly positive entries in that list, including tied positive payments at different ranks.

Given $r$, the paper's symmetric equilibrium has an ability threshold $a_{\min}(r,c_p)$: a solver enters precisely when $a\ge a_{\min}$. The expected rank reward $R_r(a)$ determines that threshold, and the paper gives an integral expression for the resulting equilibrium performance $x_r^*(a)$ (Proposition 1, p. 8). Both quantities depend on the entire announced allocation. The independent ability profile has the product law of the density on $[0,1]$. If $N$ is the number entering, the failure probability is $\Pr(N=0)$.

The firm's objective is equation (6), with failure cost $c_f\ge0$:

$$\Pi(r;c_p,c_f)=\mathbb E\!\left[\max_{1\le i\le n}\{x_r^*(A_i)\mathbf 1_{\{A_i\ge a_{\min}(r,c_p)\}}\}\right]-c_f\Pr_r(N=0).$$

Every allocation comparison recalculates $a_{\min}$, $x^*$, and the failure probability. An optimal allocation maximizes this objective over every feasible $r$, including allocations that spend less than the budget.

Formalization targets

The main target is Theorem 2, including existence of an optimum. For $c_p=0$, every positive budget and nonnegative failure cost have an optimum, and every optimum pays exactly one rank. For $c_p>0$, the corrected statement asserts thresholds $\widehat c_p>c_p$ and, for each budget $c_p<B<n c_p$, a threshold $\widehat c_f>0$ such that every optimum satisfies

$$B<\widehat c_p\ \text{or}\ c_f<\widehat c_f\quad\Longrightarrow\quad m(r^*)=1,$$ $$\widehat c_p<B\ \text{and}\ \widehat c_f<c_f\quad\Longrightarrow\quad 2\le m(r^*)\le m_p^*(B).$$

Here $m_p^*(B)$ is the largest number of equal awards that maximizes participation. The same two thresholds govern both clauses. Equality at a threshold is left open because allocations can tie there. The bound $B<n c_p$ is the paper's constrained-budget regime, stated in its discussion and used in its threshold proof (Theorem 1 and its discussion, p. 10; proof of Proposition 1, p. 23). At $n=2$, this regime may have no multi-reward case; the conditional statement retains the paper's population range.

The milestone results include the rank-probability identity (EC.3), the binomial law for the number of entrants (Proposition 2), the equal-award participation optimum (Theorem 1), attainment of the firm's maximum, and the claim that winner take all maximizes the first, performance term of $\Pi$ (Electronic Companion and proofs, pp. ec1, 9–10, 28).

What the result supplies

The theorem separates the firm's two aims in a precise way: a positive entry cost and a sufficiently consequential failure can justify paying more than the top rank, while the participation-maximizing number $m_p^*$ bounds how far the firm should spread rewards. The result is a statement about all optimal feasible allocations, not merely a comparison of a few equal-split choices. It also identifies the number of entrants through a binomial law, so the failure event has an explicit probability (Proposition 2, p. 9).

The paper presents these results and their arguments, but this mission's statements still require Lean proofs. A complete formalization would connect the rank and participation formulas to the objective evaluated on independent ability profiles, and establish existence and the design regimes. The order-statistic definitions and product-measure treatment of the ability population can be reused in other contest models.

Mathematical difficulty

The obvious thought is to maximize performance and participation separately, then compare their best allocations. That does not settle the firm's problem because changing a reward changes the entry threshold and the performance schedule at the same time. In particular, the performance term under partial entry cannot be replaced by its guaranteed-entry counterpart: entrants are selected by ability, and the selection threshold moves with the allocation. The printed proof of Theorem 2 cites a guaranteed-entry result at this point, leaving a substantive partial-entry comparison for the mission (proof of Theorem 2, pp. 27–28; Theorem EC.2, p. ec5).

Formalization scope

Lean uses natural-number ranks $1,\ldots,n$, real abilities and rewards, and the density-based measure on $[0,1]$ whose finite product gives independent solver abilities. The order-statistic CDF is a binomial sum; its empty-range value is zero. The participation threshold is the least $a\in[0,1]$ for which expected rank reward reaches $c_p$, with value one when that set is empty. The submission schedule is equation (4), and the firm's objective is the expectation in equation (6), not its later reduced integral form. A finite maximum over the $n$ solvers represents the best submission. Only positive rewards count toward $m(r)$; the unused rank-zero coordinate and rewards above rank $n$ are fixed at zero. At ability zero, division by ability is avoided in the submitted definitions.

The source's proof introduces an additional constraint that $\Pi\ge0$, even though Theorem 2 does not require it and a large failure cost can make it impossible. The mission keeps the original feasible set with $\sum r_j\le B$ and no sign restriction on $\Pi$. This prevents a formally easy but vacuous optimum claim. The strict performance milestone is labelled as a strengthening of the printed maximization claim. Contributions that establish the equilibrium characterization, measure identities, continuity and attainment, or a rigorous partial-entry performance comparison are within scope.

Selected references

• Konstantinos I. Stouras, Jeremy Hutchison-Krupat and Raul O. Chao, The Role of Participation in Innovation Contests, accepted version forthcoming in Management Science, 2021, SSRN 2924224.