Operations Research

Motivation

Online selection problems ask an algorithm to accept or reject elements as they arrive, while keeping the accepted set feasible. The decisions are irrevocable, and the arrival order can be chosen after the random activity of the elements is known. A guarantee for one constraint is therefore useful only if it remains meaningful when several constraints apply at once. In Feldman, Svensson and Zenklusen's paper, the constraints include matroid independence, matching, and knapsack capacity. A set satisfying two such requirements lies in the intersection of their feasible families. Theorem 1.9 establishes how their online guarantees combine: the two selectability factors multiply.

The result belongs to a sequence of statements in the paper. The authors first define greedy online contention resolution schemes and their selectability guarantee in Definitions 1.3–1.5. They then state the combination theorem in the introduction and identify the intersection construction in Definition 2.10. Lemma 2.11 supplies the precise selectability assertion for that construction. This mission isolates those claims so that later formalizations of specific constraints can reuse them without repeating the probability argument.

Setting

Let $N$ be a finite ground set and $\mathcal F\subseteq 2^N$ a family of feasible sets. A fractional point $x\in[0,1]^N$ determines a random active set $R(x)$: each $e\in N$ belongs to $R(x)$ independently with probability $x_e$. Thus a particular set $A\subseteq N$ has weight

$$\Pr[R(x)=A]=\prod_{e\in A}x_e\prod_{e\notin A}(1-x_e).$$

A greedy online contention resolution scheme, or greedy OCRS, chooses a down-closed family $\mathcal G_x\subseteq\mathcal F$. As active elements arrive, it accepts an element when adding that element to those already accepted remains in $\mathcal G_x$. In a randomized scheme, the choice of $\mathcal G_x$ is random and independent of $R(x)$. The family contains the empty set, as the procedure begins with no accepted elements.

An element $e$ is selectable for a realized active set $A$ and family $\mathcal G_x$ if every $I\subseteq A$ with $I\in\mathcal G_x$ still permits $e$: $I\cup\{e\}\in\mathcal G_x$. This condition covers every possible set that might have been accepted before $e$ arrives. A greedy OCRS is $(b,c)$-selectable for a relaxation $P$ when the probability of this event is at least $c$ for every $x\in bP$ and every $e\in N$. The probability includes both draws when the family is randomized. Here $b,c\in[0,1]$ and $bP=\{by:y\in P\}$.

For two feasible families $\mathcal F_1,\mathcal F_2$, the combination of their greedy OCRSs independently draws $\mathcal G_{1,x}$ and $\mathcal G_{2,x}$, then uses $\mathcal G_x=\mathcal G_{1,x}\cap\mathcal G_{2,x}$. This is a family of sets satisfying both constraints. The proof also uses $\chi_e(A,F,F')$, the indicator that $I\cup\{e\}\in F$ for every $I\subseteq A$ lying in $F'$. For selectability itself, $F'=F$.

Formalization targets

Goal: Theorem 1.9

For $P_1,P_2\subseteq[0,1]^N$, let the first scheme be $(b,c_1)$-selectable and the second $(b,c_2)$-selectable. The mission asks for a greedy OCRS on the intersection with

$$\Pr[e\text{ selectable at }x]\ge c_1c_2 \quad\text{for all }x\in b(P_1\cap P_2),\ e\in N.$$

The target records existence of the combined scheme, independent of a particular proof of its selectability. The paper also claims preservation of polynomial-time efficiency; the finite mathematical model here does not assign a complexity measure to a family sampler or membership oracle, so that clause is outside this target.

Construction: Lemma 2.11

The lemma names the combined scheme: independently draw both greedy families and use their intersection. It asserts the same $(b,c_1c_2)$ bound for that specific scheme. The earlier milestones record the two order properties of $\chi_e$ and the finite product-measure correlation inequality appearing in the lemma's proof. Their statements keep the original quantifiers over active sets and families visible.

Significance

The theorem turns guarantees for individual constraints into a guarantee for simultaneous constraints. If a matroid scheme and a matching scheme meet the same scale parameter $b$, their intersection is governed by the product of their selectability factors. The factor loss is explicit, which lets subsequent algorithmic results track it without redefining the combined scheme. The lemma additionally fixes the actual distribution over intersected families, avoiding ambiguity about how two randomized procedures are coupled.

Mathlib already provides a general finite FKG inequality, but it does not state the paper's OCRS objects, the selectable event, or the intersection theorem. This mission adds those interfaces and the specialized correlation statement. The source results are proved in the cited paper; the local theorem files in this proposal are statements for later machine-checked proofs. A complete formalization would connect the finite active-set weights to Mathlib's lattice correlation theorem and then establish the randomized family bookkeeping. The finite probability definitions can also serve other OCRS results in the same paper.

Difficulty

The obvious argument would multiply the two probabilities that $e$ is selectable for the separate families. Both events depend on the same active set $R(x)$, so they are not independent even when the families are drawn independently. Moreover, selectability for the intersection checks only sets belonging to both families, whereas the original bounds check each family separately. The formal statements must keep these two dependencies distinct. The paper's two monotonicity claims and its FKG display identify the needed intermediate assertions, but their use with an arbitrary random choice of families still requires careful finite-sum reasoning.

Formalization scope

The ground set is a finite Lean type and subsets are Finsets. Feasibility is a predicate on those finite sets. Fractional points are real-valued functions, and each input relaxation is represented as a set of such functions with an explicit coordinate bound $0\le y_e\le1$. The scale and selectability parameters belong to $[0,1]$. The point $x$ ranges over $b(P_1\cap P_2)$, not over an independently chosen intersection of scaled sets, so the case $b=0$ retains the paper's meaning. The finite products define the law of $R(x)$; no measure-theoretic integral is used.

A randomized scheme is a probability weight on possible greedy families for every input point. The combined weight is the product of the two original weights summed over pairs with the required intersection, expressing independent draws. The family distribution is independent of the active-set draw. This sampling convention is necessary for the stated product guarantee and is made explicit here although Definition 2.10 does not spell it out. Each greedy family contains $\varnothing$ and lies in its own feasible family. These requirements exclude the empty-family and unconstrained-family encodings that would make selectability trivial. The unit-cube bounds prevent negative active-set weights.

The Lean declarations focus on the finite selectability guarantee. They abstract a polytope by its set of fractional points and use the paper's unit-cube condition; they do not formalize a polyhedral representation or test that its binary points equal the feasible sets. A full development of the paper's algorithmic setting would additionally represent online arrival orders, family sampling algorithms, membership oracles, and polynomial running time. Contributions establishing the finite probability lemmas, the specialized FKG statement, and Lemma 2.11 are directly useful here. The general active-set and selectability definitions are reusable across the paper's other missions.

Selected references

• Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes, arXiv preprint, 2015, arXiv:1508.00142v2. Definitions 1.3–1.5, Theorem 1.9, Definition 2.10 and Lemma 2.11.
• Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing 50(2), 2021, DOI:10.1137/18M1226130. The mission's statement indices follow the arXiv version above.

Motivation

In online selection, items reveal information one at a time, and each decision to accept an item is irrevocable. A matroid constraint permits some subsets and excludes others; it covers choices such as selecting linearly independent vectors or acyclic edges. A fractional solution can assign an acceptance probability to each item, but independent activations can produce a set that violates the constraint. An online contention resolution scheme (OCRS) turns these activations into a feasible selection while respecting the order in which items arrive. The matroid result of Feldman, Svensson and Zenklusen gives a guarantee that survives even when an adversary knows all random outcomes before choosing the arrival order.

This mission concerns the paper's matroid theorem, Theorem 2.1. The same paper develops schemes for matching and knapsack constraints and a rule for combining schemes for intersecting constraints. Those results are separate missions in this series. Here the central question is how much of a fractional matroid point can be retained by a deterministic greedy rule as each active item is revealed.

Setting

Let $N$ be a finite ground set and let $M$ be a matroid on $N$. Its independent subsets form a down-closed family $\mathcal F$: if $I$ is independent, every subset of $I$ is independent. The rank $r(S)$ of $S\subseteq N$ is the maximum size of an independent subset of $S$. The matroid independence polytope is

$$P_{\mathcal F}=\left\{x\in\mathbb R^N_{\ge0}:x(S):=\sum_{e\in S}x_e\le r(S)\text{ for all }S\subseteq N\right\}.$$

Its points have $0\le x_e\le1$. For a point $x$, the active set $R(x)$ contains each $e$ independently with probability $x_e$. A deterministic greedy OCRS assigns a down-closed family $\mathcal F_x\subseteq\mathcal F$ to $x$ and accepts an active element when adding it to the already accepted set stays in $\mathcal F_x$. The empty set belongs to every $\mathcal F_x$. The rule depends on $x$ before the active set and arrival order are revealed.

An element $e$ is selectable for an active set $A$ if $I\cup\{e\}\in\mathcal F_x$ for every $I\subseteq A$ with $I\in\mathcal F_x$. A greedy OCRS is $(b,c)$-selectable if this event has probability at least $c$ for every $x\in bP_{\mathcal F}$ and every $e\in N$. The event implies that $e$ can be added regardless of which eligible active elements arrived first. These definitions are from §1.1 of the paper.

Formalization targets

Matroid OCRS

For every $b\in[0,1]$ and every finite loopless matroid $M$, the target is a deterministic greedy OCRS with

$$\Pr\left[I\cup\{e\}\in\mathcal F_x\text{ for all }I\subseteq R(x),\ I\in\mathcal F_x\right]\ge 1-b \quad\text{for every }x\in bP_{\mathcal F},\ e\in N.$$

The loopless condition is a disclosed correction to the printed Theorem 2.1: a loop cannot belong to any independent singleton, so its selectability is zero. The printed bound would demand positive selectability for that loop whenever $b<1$. The theorem keeps the paper's constant $1-b$ exactly.

Supporting targets

The milestones reproduce six statements from §2.1–2.1.1, in attack order: validity of a family defined by a chain $\varnothing=N_\ell\subsetneq\cdots\subsetneq N_0=N$ of matroid minors (independence of the union of layer-wise independent sets is Soto, Theorem 5.1); a characterization of selectability through span in one layer; monotonicity of the first chain set as coordinates of $x$ increase; the description of the base polytope $P_{\mathcal B}=\{x\in P_{\mathcal F}:x(N)=r(N)\}$ as the set of maximal vectors of $P_{\mathcal F}$; the weighted span bound of Lemma 2.4,

$$\sum_{e\in N}x_e\Pr[e\in\operatorname{span}(R(x)\cup S)]\le b\cdot\bigl(x(N)+(1-b)\,r(S)\bigr),$$

strict when $S\neq\varnothing$; and the proper-inclusion conclusion $S\subsetneq N$ of Corollary 2.5. They expose the distinct matroid and probability claims on which the main theorem rests.

Significance

The theorem gives a fixed greedy family for each fractional point, with a per-element probability guarantee that is independent of the arrival order. Offline contention resolution schemes for matroids were introduced by Chekuri, Vondrák and Zenklusen; the online, almighty-adversary version here is stronger. A solver can use that guarantee as the matroid component in larger online selection problems. In the source paper it feeds the intersection and application results; those applications require further models and statements beyond this mission. The factor $1-b$ makes the tradeoff explicit: using a more heavily scaled fractional point raises the risk of contention.

The result is proved in the cited paper. This mission asks for a machine-checked Lean proof of its corrected statement and the source's supporting claims. A successful development would add reusable finite representations of independent activation, matroid polytope inequalities, span probabilities, and chain families. It would also make the loop boundary explicit, preventing a formally false version of the printed theorem from being published as a target.

Difficulty

Independent activation does not itself respect matroid independence. A greedy family that simply contains every independent set can make an element unavailable after earlier active elements are accepted, and the arrival order can expose the worst such history. The central issue is therefore a uniform selectability event: the same element must remain addable after every feasible subset of the active set. The paper measures that obstruction through spans in successive matroid minors. The first chain set must be proper so that the construction can continue, which is why the strict part of the weighted span inequality matters.

Formalization scope

The ground set is a finite Lean type, subsets are Finsets, and Mathlib's Matroid supplies independence, closure, contraction and restriction. Matroid rank is converted from Mathlib's extended natural rank to a real number; finiteness makes this conversion finite on every subset. The independence and base polytopes are defined by the paper's inequalities. The scalar multiple $bP$ is pointwise set scalar multiplication, including $b=0$.

Probabilities are finite sums of product weights over all active sets. In particular, the event in Lemma 2.4 uses $\operatorname{span}(R(x)\cup S)$, whereas the recurrence defining $S$ uses $\operatorname{span}((R(x)\cup S_i)\setminus\{e\})$. These are separate definitions. Every point used for activation lies in $[0,1]^N$, as enforced by the polytope and $b\in[0,1]$. The base-polytope condition on Corollary 2.5 is the standing assumption stated before the lemma in the source.

The loopless condition applies to the goal, to Corollary 2.5, and to the strict clause of Lemma 2.4 only; its non-strict clause, the chain statements and the monotonicity statement hold for every matroid and are stated without it. Three trivializing formalizations are ruled out: every greedy family must contain the empty set, so an empty family cannot satisfy selectability vacuously; every member of a greedy family must be independent in $M$, so $\mathcal F_x=2^N$ is not admissible; and every point used for activation lies in $[0,1]^N$, so $\Pr[R(x)=A]$ is a genuine probability. The quantified scheme depends only on $x$, and its success condition ranges over every feasible subset of the realized active set. Contributions that establish the chain family's independence, finite probability identities, and rank or closure facts are within scope. Polynomial-time implementation and the Monte Carlo estimates of Lemma 2.6 are outside this mission's mathematical target.

Selected references

• Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015; published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021. Preprint.
• Chandra Chekuri, Jan Vondrák and Rico Zenklusen, Submodular Function Maximization via the Multilinear Relaxation and Contention Resolution Schemes, SIAM Journal on Computing, 2014. arXiv:1105.4593.
• José A. Soto, Matroid Secretary Problem in the Random-Assignment Model, SIAM Journal on Computing, 2013. arXiv:1007.2140.

Motivation

Minimum-cost flow is a standard model for routing a quantity through a network while paying a cost on each arc. Unit capacities arise when each input arc can carry at most one unit; they include flow formulations of several matching and assignment problems. Goldberg, Kaplan, Hed and Tarjan analyze a cost-scaling algorithm for this setting. Their second-phase argument depends on a bound on the excess left in a pseudoflow when every excess vertex has undergone enough potential increases. This mission formalizes that bound, Lemma 5 of their STACS 2015 paper. The published paper gives an $O(\min\{m^{1/2},n^{2/3}\}\,m\log(nC))$ running-time bound for its unit-capacity algorithm; the running-time statement itself is outside this mission.

Setting

A network has a finite vertex set $V$ and an arc set $E$ that contains both orientations of each input arc. Write $n=|V|$. Every input arc has capacity one; its reverse has capacity zero and opposite cost. Write $m$ for the number of input arcs, so $|E|=2m$. The paper assumes no parallel or antiparallel input arcs, allowing an arc to be identified by its ordered endpoints. Costs are antisymmetric between orientations.

A pseudoflow $f$ assigns an antisymmetric quantity to each arc and respects its capacity. Its excess at $v$ is the sum $e_f(v)$ of incoming flow. Positive excess means that $v$ has flow to discharge; negative excess is a deficit. A circulation is a pseudoflow with zero excess at every vertex. An arc is residual for $f$ when its residual capacity $u_f(v,w)=u(v,w)-f(v,w)$ is positive. For vertex prices $p$, its reduced cost is $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal at $p$ when every residual arc has reduced cost at least $-\varepsilon$. These are the paper's conventions on p. 408.

At the start of a cost scale, let $f'$ be a circulation that is $2\varepsilon$-optimal at prices $p'$. During the scale, $f$ is a pseudoflow that is $\varepsilon$-optimal at prices $p$. The potential increase in scale units is $d(v)=(p(v)-p'(v))/\varepsilon$. Put $\lambda=\min\{\sqrt m,n^{2/3}\}$. The second phase begins when every excess vertex has $d(v)\ge\lambda$; the paper also states that every deficit then has $d(v)=0$ and that the levels $d(v)$ are integral. The remaining excess is $X(f)=\sum_{v:e_f(v)>0}e_f(v)$.

The comparison graph has arcs $E^+=\{(v,w)\in E:f'(v,w)>f(v,w)\}$ and vertices $V$. An excess–deficit cut $Y\subseteq E^+$ meets every path in this graph from an excess vertex to a deficit vertex. Thus a cut is measured among comparison arcs, not among arbitrary arcs of the original network. Lemmas 3 and 4 of the paper establish the level and cut bounds on which the excess estimate rests.

Formalization targets

The goal is Lemma 5 on p. 410, stated with both constants obtained in its proof. Under the cost-scale conditions above, and the divisibility conventions in footnotes 5–6, its two cases are

$$\lambda=\sqrt m\quad\Longrightarrow\quad X(f)\le 3\lambda,$$ $$\lambda=n^{2/3}\quad\Longrightarrow\quad X(f)\le36\lambda.$$

The second case also assumes that six divides the integer $\lambda$; the first uses divisibility by three. The goal keeps the two conclusions separate so that the stronger $3\lambda$ bound is retained when $\sqrt m$ determines the scale. Its milestone list follows the paper: Lemma 3 bounds $d(v)-d(w)$ by three on an arc of $E^+$; Lemma 4 bounds total excess by a cut; and the proof of Lemma 5 supplies the cut bands and the two size estimates. The bands use the exact three-level and six-level ranges printed on p. 410.

Significance

The result connects a condition on price increases to a numerical bound on the amount of flow still needing discharge. Combined with the paper's time per unit of remaining excess, this is the bound needed for its second-phase running-time estimate. The two regimes show how the same cost-scale state can be controlled by either the number of input arcs or the number of vertices. Without the excess bound, the paper's argument gives no comparable limit on the remaining work at the phase transition.

The paper proves Lemma 5, but this particular unit-capacity excess argument has no matching theorem in the platform catalog checked for this mission. The network, circulation and pseudoflow interfaces are already published as reusable definitions from earlier cost-scaling work. A completed machine-checked development would add the cut argument and band counts to those interfaces. Those facts can also support other analyses that compare an entry circulation with an intermediate pseudoflow; this mission does not claim to formalize the algorithm's entire execution or its running-time model.

Difficulty

The main obstacle is linking local price inequalities to a global bound on excess. A reduced-cost inequality controls a single residual arc, while excess may move through a path and is measured over many vertices. The comparison graph $G^+$ is essential: on a residual arc outside $E^+$, the level difference used by Lemma 3 is not available. Counting all residual arcs as if they were comparison arcs would therefore not justify the cut bound. There is a separate counting issue: the represented network has both directions of each input arc, so using $|E|$ for $m$ changes the constant in the square-root case.

Formalization scope

Lean represents the network by a finite symmetric arc set with real capacities and antisymmetric real costs. A local unit-capacity predicate marks each reverse pair as capacities $(1,0)$ or $(0,1)$; $m$ counts the capacity-one orientations. Flows are real valued as on p. 408. Integer costs on that page are generalized to real costs because Lemmas 3–5 use only antisymmetry and reduced-cost inequalities. No result here depends on cost integrality.

The formalization takes the cost-scale state as hypotheses: $\varepsilon>0$, entry circulation and $2\varepsilon$-optimality, current $\varepsilon$-optimality, integral levels, level at least $\lambda$ at excess vertices, and zero level at deficits. It takes $\lambda$ as a natural number equal to $\min\{\sqrt m,n^{2/3}\}$ and records the paper's divisibility simplifications. The indexed pigeonhole milestones also require $\lambda>0$ so their index ranges are nonempty; the goal includes the zero-arc boundary without requiring an index. Cuts use reachability after deleting a subset of $E^+$, equivalent to meeting every excess-to-deficit path. The proof of Lemma 5 prints “cut in $G_f$”; the formalized claim uses $G^+$, the graph for which Lemma 3 gives the required level control and Lemma 4 states its bound.

The definition layer, path-cut lemma and finite counting arguments are the reusable infrastructure. Contributions that establish these exact statements, their necessary elementary flow identities, or a machine-checked goal proof are in scope. Counting $m$ with reverse arcs, allowing cuts outside $E^+$, using arbitrary real levels in place of integral ones, or replacing both cases by the weaker $36\lambda$ bound does not express this target.

Selected references

• A. V. Goldberg, H. Kaplan, S. Hed and R. E. Tarjan, Minimum Cost Flows in Graphs with Unit Capacities, 32nd International Symposium on Theoretical Aspects of Computer Science, LIPIcs 30, pp. 406–419, 2015. doi:10.4230/LIPIcs.STACS.2015.406.

Motivation

Online sellers of loans, insurance, travel and retail goods observe data about each arriving customer before quoting a price. Using that data to price individually is attractive only if the seller can learn, from its own sales, how demand responds to price for customers with given characteristics. Two features make this hard in practice. The number of recorded characteristics $d$ is often large, possibly larger than the selling horizon $T$, while only a few of them matter. And price sensitivity is itself heterogeneous: different customers respond to the same price change differently.

Ban and Keskin (Management Science 67(9), 2021) model both features and ask how fast the revenue lost to learning can grow. Their answer is that a seller who learns with lasso-regularized quasi-likelihood estimation and occasional price experiments loses revenue of order $s\sqrt T$ up to logarithmic factors, where $s$ is the number of relevant characteristics, and that no policy can do better than order $s\sqrt T$. This mission formalizes the upper bound for the general (nonlinear-link) model with unknown sparsity, Theorem 3 of the paper.

Setting

In each period $t = 1, 2, \dots, T$ a customer arrives with a raw feature vector $Z_t \in \mathbb R^d$. The $Z_t$ are i.i.d., take values in a compact set $\mathcal Z$ inside a ball of radius $z_{\max}$, have mean zero and positive definite covariance $\Sigma_Z$. The seller sees the augmented vector $X_t = [1; Z_t] \in \mathbb R^{d+1}$, charges a price $p_t \in [\ell, u]$ with $0 < \ell < u$, and observes the demand

$$D_t = g\big(\alpha \cdot X_t + (\beta \cdot X_t)\, p_t\big) + \varepsilon_t .$$

Here $\theta = (\alpha, \beta)$ is an unknown parameter in a compact rectangle $\Theta \subset \mathbb R^{2(d+1)}$, the link $g$ is known, differentiable and increasing with $\tilde\ell \le g' \le \tilde u$ on the relevant domain, and the demand shocks $\varepsilon_t$ form a sub-Gaussian martingale difference sequence. The term $\beta \cdot X_t$ is the customer's own price sensitivity. With $u(p, x) = [1; p] \otimes x$ the argument of $g$ is $\theta \cdot u(p, x)$.

The sparsity of $\theta$ is $s = |\mathcal S|$, $\mathcal S = \{i : \alpha_i \neq 0\} \cup \{i : \beta_i \neq 0\}$. The seller does not know $\mathcal S$.

The expected revenue of price $p$ is $r(p, \theta, x) = p\, g(\theta \cdot u(p,x))$, and the clairvoyant price $\varphi(\theta, x)$ maximizes it; it is assumed to lie in the interior of $[\ell, u]$ for $\theta \in \Theta$, $x \in \mathcal X = \{1\} \times \mathcal Z$. The regret of a policy over $T$ periods is

$$\Delta^\pi_\theta(T) = \mathbb E\Big[\sum_{t=1}^T r^*(\theta, X_t) - r(p_t, \theta, X_t)\Big], \qquad r^*(\theta,x) = r(\varphi(\theta,x),\theta,x).$$

The policy ILQX$(m_1, m_2, \lambda)$ charges the experimental price $m_1$ in periods $M_1 = \{1, 4, 9, \dots\}$ and $m_2$ in periods $M_2 = \{2, 5, 10, \dots\}$, and otherwise charges $\varphi(\mathcal P_\Theta \hat\theta_t, X_t)$, where $\hat\theta_t$ maximizes the lasso-penalized quasi-likelihood

$$Q_{t-1}(\tilde\theta, \lambda_t) = \sum_{k=1}^{t-1} \chi_k \int_{D_k}^{g(\tilde\theta \cdot u_k)} \frac{D_k - y}{g'(g^{-1}(y))}\, dy - \lambda_t \|\tilde\theta\|_1$$

over the experimental periods ($\chi_k = \mathbb I\{k \in M_1 \cup M_2\}$), and $\mathcal P_\Theta$ is the projection onto $\Theta$. The regularization level is $\lambda_{t+1} = \tilde c\, t^{1/4} \sqrt{\log d + \log t}$ for a constant $\tilde c > 0$.

Formalization targets

Goal: Theorem 3

There is a finite constant $\tilde C > 0$ such that

$$\Delta^\pi_\theta(T) \le \tilde C\, s \sqrt T\, (\log d + \log T) \qquad \text{for all } \theta \in \Theta,\ T \ge 2 .$$

$\tilde C$ is fixed with the model and is uniform over $\Theta$; since $s = s(\theta)$ varies over $\Theta$, the factor $s$ carries content.

Milestones

1. The counting property of the schedule (7): for $t \ge 5$ each experimental price is charged at least $\tfrac14 \sqrt t$ times in periods $1, \dots, t$.
2. Lemma 3, the estimation error of the lasso quasi-likelihood estimate:

$$\mathbb P\Big\{\|\hat\theta^{(\mathrm{lasso})}_{t+1}(\lambda_{t+1}) - \theta\|^2 \le \rho_3 \frac{s(\log d + \log t)}{\sqrt t}\Big\} \ge 1 - \kappa_3 \frac{s(\log d + \log t)}{\sqrt t}, \qquad t \ge t_1 .$$

Significance

Theorem 3 says that a seller facing many potentially relevant customer characteristics, without knowing which matter and under a nonlinear demand link such as logit, loses revenue at a rate governed by the number $s$ of relevant characteristics and only logarithmically by the total number $d$. Combined with the paper's $s\sqrt T$ lower bound (Theorem 1, for the linear model), it makes ILQX first-order optimal up to logarithmic factors. An unregularized policy would pay order $d\sqrt T$, which is linear in $T$ when $d$ exceeds $\sqrt T$.

The paper's proofs are in its electronic companion, which this mission does not reproduce; no machine-checked version of the result exists. A complete formalization would also produce a reusable high-probability error bound for lasso-regularized quasi-likelihood estimation under adaptively collected data (Lemma 3), and a machine-checked model of feature-based dynamic pricing on which related policies can be stated.

Difficulty

The estimation error must be controlled on data collected by the policy itself. The design vectors $u_k = [1; m_{i(k)}] \otimes X_k$ use only two prices, so the information about the price sensitivity accrues only from the $\Theta(\sqrt t)$ experimental periods. Standard lasso error bounds assume a fixed or i.i.d. design and a restricted-eigenvalue condition on it; here a restricted-eigenvalue-type property of the random Kronecker design must be derived from $\Sigma_Z \succ 0$ and $m_1 \ne m_2$, and the noise enters through a martingale whose conditional law may depend on past prices. The quasi-likelihood is not a least-squares objective, so the curvature comes from the bounds $\tilde\ell \le g' \le \tilde u$, which hold only on the bounded domain $\{\theta \cdot u(p,x) : \theta \in \Theta\}$ and not at an unconstrained estimate. Finally, the regret bound has to turn a squared-error bound holding with probability $1 - O(s \log(dt)/\sqrt t)$ into an expected revenue loss, which requires the revenue loss to be second order in the parameter error at an interior optimum.

Formalization scope

• Coordinates. $x \in \mathbb R^{d+1}$ is Fin (d+1) → ℝ with the intercept at index 0; $\theta$ is Fin 2 × Fin (d+1) → ℝ with $\theta(0,i) = \alpha_i$, $\theta(1,i) = \beta_i$. Periods are 1-based. $d \ge 1$.
• Objective. The integrated form $\sum_k \chi_k \big(D_k\,(\tilde\theta \cdot u_k) - \int_0^{\tilde\theta \cdot u_k} g\big) - \lambda \|\tilde\theta\|_1$, which differs from the paper's (17) by a term not depending on $\tilde\theta$ and therefore has the same maximizers.
• Estimator. Any measurable selection that is a maximizer whenever one exists; the theorems hold for every such selection. The paper's claim that (17) is strictly concave with a unique maximizer fails when $2(d+1)$ exceeds the rank of the design.
• Policy. The price is defined by strong recursion over the realized history; the estimator sees $\theta$ only through the realized demands.
• Regret is a lower Lebesgue integral of nonnegative losses; conditional moments of the shocks use the conditional Lebesgue expectation; probabilities are compared in $[0, \infty]$.
• Standing assumptions formalized: i.i.d. measurable features in a compact $\mathcal Z$ inside a Euclidean ball, mean zero, positive definite $\Sigma_Z$; fresh customers ($Z_{t+1}$ independent of the past); sub-Gaussian martingale-difference shocks; $m_1 \ne m_2$ in $[\ell, u]$; $g$ differentiable and increasing with derivative bounds on the relevant domain (endnote 2 states them as a consequence, which is false; here they are a hypothesis); $\varphi$ an unconstrained revenue maximizer in $(\ell, u)$ whose pricing map after projection and feature augmentation is measurable. The processes are constrained only at the used periods $t\ge1$.
• Added hypotheses, per $\theta$: $s(\theta) \ge 1$ (the paper's $s \in \{1, \dots, d+1\}$), and almost surely every realized demand lies in the closure of the range of $g$, which guarantees that a maximizer of (17) exists (true for the linear link and for binary demand under a logit link).
• Not formalized: the paper's support condition on continuous features; Remark 7's independence of $\tilde C$ from $d$; dependence of the shock law on $\theta$ (the shocks are one fixed process).
• Ruled-out trivializations. The regret cannot vanish by non-integrability; the estimator cannot be an arbitrary function, since it must maximize the objective; $\tilde C$ and $\kappa_3, \rho_3, t_1$ are chosen before $\theta$, so they cannot absorb $s$; the hypotheses are jointly satisfiable (a linear-link instance with $d = 1$ is checked).

Contributions welcome: existence of a measurable maximizer of the objective, the counting lemma, and supporting lemmas for Lemma 3 and the regret bound.

Selected references

• G.-Y. Ban and N. B. Keskin, Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity, Management Science 67(9):5549–5568, 2021. https://doi.org/10.1287/mnsc.2020.3680
• A. V. den Boer and B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
• N. B. Keskin and A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014. https://doi.org/10.1287/opre.2014.1294
• A. Javanmard and H. Nazerzadeh, Dynamic Pricing in High-Dimensions, Journal of Machine Learning Research 20(9):1–49, 2019. https://jmlr.org/papers/v20/17-357.html

Motivation

A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.

Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.

Setting

The hidden state space is $X=\{1,2\}$ and the observation space is $Y=[0,1]$ with Lebesgue probability measure $m$. The action space is $A=\{0\}\cup\{1/n:n=1,2,\ldots\}$, equipped with the topology inherited from $\mathbb R$. The state does not move: its transition law $P(\cdot\mid x,a)$ is the point mass at $x$ for every action. Its continuity in total variation is immediate from this fixed-state behavior.

At hidden state 1 the observation law is always $m$. At hidden state 2, action zero also produces $m$. Under action $1/n$, state 2 produces a law $m^{(n)}=f^{(n)}m$. The density $f^{(n)}$ equals zero on the open left half of each cell in the $2^n$-part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as $n$ grows, and the paper establishes $m^{(n)}(C)\to m(C)$ for every fixed Borel set $C$. Thus the observation kernel $Q(\cdot\mid a,x)$ is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.

A belief $z\in\mathcal P(X)$ assigns a probability to each hidden state. For a current belief $z$ and an action $a$, the joint law $R(\cdot\mid z,a)$ covers the next state and its observation, and $R'(\cdot\mid z,a)$ is the observation marginal. A filter $H(z,a,y)$ is a conditional law of the next state given observation $y$: it satisfies the disintegration identity (3.3). The belief transition $q_H(\cdot\mid z,a)$ is the law of the random posterior $H(z,a,y)$ when $y$ has law $R'(\cdot\mid z,a)$. These objects are defined in (3.1)–(3.5) of the paper. Different versions of $H$ agree only almost everywhere for each current belief and action, yet they yield the same belief transition.

Formalization targets

Example 4.1: failure of weak belief continuity

At the uniform belief $z=(1/2,1/2)$, action zero reveals nothing, while every positive-index action produces the same two-point posterior law:

$$q_H(\cdot\mid z,0)=\delta_z,\qquad q_H(\cdot\mid z,1/n)=\tfrac34\delta_{(1/3,2/3)}+\tfrac14\delta_{(1,0)} \quad(n\ge1).$$

The mission's goal asserts that $P$ is total-variation continuous, $Q$ is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as $1/n\to0$. It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of $Q$, the two posterior values almost everywhere, and the explicit laws of $q_H$.

Significance

The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.

A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.

Difficulty

Setwise continuity controls $Q(C\mid a,x)$ for each fixed Borel set $C$. A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with $n$, so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of $Q$ to weak convergence of $q_H$.

The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every $y$ would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of $H$.

Formalization scope

Lean represents $X$ by Fin 2, with 0 for the paper's state 1 and 1 for state 2; $Y$ by unitInterval; and $A$ by the specified subtype of $\mathbb R$. Positive integers are a subtype of $\mathbb N$, so the density and the action $1/n$ are never evaluated at $n=0$. The measure $m$ is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition $P$ and observation law $Q$ use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete $Q$ and existence of a valid $H$, guarding the universal filter clause against vacuity.

Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of $q_H$ carries the Borel σ-algebra of the weak topology on $\mathcal P(X)$, stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in $y$ for fixed $(z,a)$ in both structures. Joint measurability in $(z,a,y)$ is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.

No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on $A$, or a claim for only one version of $H$ would change the counterexample and is excluded by the definitions and goal.

Selected references

• E. A. Feinberg, P. O. Kasyanov, and M. Z. Zgurovsky, Partially Observable Total-Cost Markov Decision Processes with Weakly Continuous Transition Probabilities, Mathematics of Operations Research 41(2), 2016; arXiv:1401.2168v2. This mission follows the pinned preprint's numbering and pages.

Motivation

Games with many interacting players appear in economics, epidemiology and network engineering: firms competing in a market, individuals deciding whether to vaccinate, agents in a social network choosing an effort level. When every player interacts with every other player symmetrically, mean field game theory replaces the finite game by a limit with a continuum of players. Real interactions are rarely symmetric: who influences whom is described by a network, and large networks are described in the limit by a graphon (Lovász, Large networks and graph limits, 2012).

Graphon games combine the two ideas. Parise and Ozdaglar (2018) studied deterministic graphon games with continuous strategy sets. Carmona, Cooney, Graves and Laurière (2019) introduced idiosyncratic random shocks, giving a stochastic graphon game in which each player's state is perturbed by independent noise, and proved existence, uniqueness and stability of Nash equilibria as well as convergence of finite network games to the graphon limit. This mission formalizes their existence theorem (Theorem 3.15).

Setting

The players form the interval $I=[0,1]$ with Lebesgue measure $\lambda_I$. Each player $x\in I$ chooses an action $\alpha_x\in A=\mathbb R$; a strategy profile is a function $\alpha\in L^2(I)$, defined up to $\lambda_I$-null sets.

A graphon is a symmetric, Borel-measurable function $w:I\times I\to\mathbb R$ with $\int_{I\times I}w(x,y)^2\,dx\,dy<\infty$. It acts on $L^2(I)$ through the graphon operator

$$[\mathbf Wg]_x=\int_I w(x,y)\,g(y)\,dy,\qquad \|\mathbf W\|=\sup_{\|\varphi\|_{L^2(I)}=1}\|\mathbf W\varphi\|_{L^2(I)}.$$

A state map $b:\mathbb R\times\mathbb R\to\mathbb R$ and a noise law $\mu_0$ on $\mathbb R$ define the state $X_{\alpha,z,\xi}=b(\alpha,z)+\xi$ of a player who takes action $\alpha$, feels aggregate $z$, and receives shock $\xi\sim\mu_0$. Assumption 1 asks that $|b(\alpha,z)-b(\alpha',z')|^2\le c_\alpha|\alpha-\alpha'|^2+c_z|z-z'|^2$ and that $\mu_0$ has mean zero and a finite second moment.

The aggregate $\mathbf Z\alpha$ felt by the players under a profile $\alpha$ is the solution $z\in L^2(I)$ of

$$z_x=\int_I w(x,y)\,b(\alpha_y,z_y)\,dy\qquad\text{for }\lambda_I\text{-a.e. }x.\tag{6}$$

A player choosing $\alpha$ against aggregate $z$ pays $J(\alpha,z)=\int f(b(\alpha,z)+\xi,\alpha,z)\,\mu_0(d\xi)$. Assumption 4 asks that $J(\cdot,z)$ be continuously differentiable and $\ell_c$-strongly convex uniformly in $z$, and that $\partial_\alpha J$ be $\ell_J$-Lipschitz in $z$. Assumption 5 asks that $b$ be bounded: $|b(\alpha,z)|\le c_0$ for some finite $c_0>0$. The best response $[\mathbf Bz]_x$ is the unique minimizer of $\alpha\mapsto J(\alpha,z_x)$.

A Nash equilibrium is a profile $\hat\alpha\in L^2(I)$ such that, for $\lambda_I$-a.e. player $x$ and every action $\beta$,

$$J(\hat\alpha_x,(\mathbf Z\hat\alpha)_x)\le J(\beta,(\mathbf Z\hat\alpha)_x).$$

Formalization targets

Goal: Theorem 3.15 (existence)

$$\text{Assumptions 1, 4, 5 and }\sqrt{c_z}\,\|\mathbf W\|<1\ \Longrightarrow\ \text{there is at least one Nash equilibrium.}$$

The statement fixes no constants and asserts no uniqueness.

Milestones

1. Proposition 3.1: under $\sqrt{c_z}\|\mathbf W\|<1$, (6) has a unique solution in $L^2(I)$ for every $\alpha\in L^2(I)$.
2. Lemma 3.7: $\|\mathbf Bz^1-\mathbf Bz^2\|_{L^2}\le(\ell_J/\ell_c)\|z^1-z^2\|_{L^2}$.
3. Lemma 3.16, (15): $\|\mathbf Z\alpha^1-\mathbf Z\alpha^2\|_{L^2}\le\dfrac{\sqrt{c_\alpha}\|\mathbf W\|}{1-\sqrt{c_z}\|\mathbf W\|}\|\alpha^1-\alpha^2\|_{L^2}$.
4. Proof of Theorem 3.15, first claim: with $\chi=c_0$ and $B_\chi=\{g\in L^2(I):\|g\|\le\chi\}$, every aggregate lies in $\mathbf W(B_\chi)$.
5. Proof of Theorem 3.15, second claim: $\mathbf W(B_\chi)$ is relatively compact in $L^2(I)$.

Significance

The existence theorem holds under mild hypotheses: unlike the uniqueness result of the same paper (Proposition 3.17), it needs no smallness condition linking $\ell_J/\ell_c$, $c_\alpha$ and $\|\mathbf W\|$. Boundedness of the state map takes its place. Existence of a graphon equilibrium is the starting point for the paper's §4, where graphon equilibria are shown to be limits of equilibria of finite network games and to yield $\epsilon$-Nash equilibria for them.

The result is proved in the paper; no part of it is machine-checked. A complete formalization yields reusable pieces beyond this mission: square-integrable kernel operators on $L^2[0,1]$ with their operator norm, the Hilbert–Schmidt compactness of such operators, Lipschitz dependence of minimizers of uniformly strongly convex functions on a parameter, and Schauder's fixed-point theorem on a Banach space, which is not in Mathlib.

Difficulty

A contraction argument does not apply: the best-response-of-aggregate map $\mathbf B\mathbf Z$ is Lipschitz with constant $\frac{\ell_J}{\ell_c}\cdot\frac{\sqrt{c_\alpha}\|\mathbf W\|}{1-\sqrt{c_z}\|\mathbf W\|}$, which may exceed $1$ under the hypotheses of the theorem. Existence therefore rests on a compactness fixed-point theorem in the infinite-dimensional space $L^2(I)$. That requires compactness of the integral operator $\mathbf W$, which Mathlib does not provide for kernel operators, and Schauder's theorem itself, which Mathlib does not have. A bounded convex set in $L^2(I)$ is not compact, so Brouwer-type finite-dimensional arguments do not transfer directly.

Formalization scope

All statements live in the namespace GraphonGames.Existence and share one definitions file.

• $I$ is Mathlib's unitInterval with volume. Profiles and aggregates are functions $I\to\mathbb R$ with MemLp _ 2 volume; equalities between them are almost-everywhere equalities.
• The action set is $\mathbb R$.
• $\|\mathbf W\|$ is the supremum, in $[0,\infty]$, of $\|\mathbf W\varphi\|_{L^2}$ over $\|\varphi\|_{L^2}=1$; the graphon condition makes it finite, and the hypothesis $\sqrt{c_z}\|\mathbf W\|<1$ uses its real value.
• The aggregate is a predicate: $z$ is an aggregate of $\alpha$ when $z\in L^2(I)$ and (6) holds a.e. Remark 3.3's identity $\mathbf Z\alpha=\mathbf W[b(\alpha,\mathbf Z\alpha)]$ is then the definition itself, the noise having mean zero.
• The best response is a choice of minimizer, which exists and is unique under Assumption 4.
• Pinned definition. The paper defines equilibrium (Definition 3.4) as a fixed point of a best response built on a rich Fubini extension, and states in Proposition 3.6 that under Assumption 4 this is equivalent to the a.e. best-response inequality above. The formalization takes that inequality as the definition. Fubini extensions and the exact law of large numbers (Proposition 3.2) are not formalized.
• Norm inequalities are stated in $[0,\infty]$, so an infinite left-hand side cannot make a bound vacuous.

Trivializing encodings are excluded: the operator norm is not a real supremum that could collapse to $0$; an equilibrium must come with its aggregate solving (6), be square-integrable, and beat every action $\beta\in\mathbb R$ for almost every player; and no norm is converted to a real number where it could be infinite.

The results of §4 (Theorems 4.3, 4.7, 4.9 on finite network games) and the uniqueness and stability results (Proposition 3.17, Theorem 3.20) are not posed in this mission. Contributions welcome include Schauder's fixed-point theorem, the compactness of Hilbert–Schmidt integral operators on $L^2$, and the contraction argument behind Proposition 3.1.

Selected references

• R. Carmona, D. B. Cooney, C. V. Graves, M. Laurière, Stochastic Graphon Games: I. The Static Case, arXiv:1911.10664v1, 2019; Mathematics of Operations Research 47(1), 2022. https://arxiv.org/abs/1911.10664
• F. Parise, A. Ozdaglar, Graphon games, arXiv:1802.00080, 2018. https://arxiv.org/abs/1802.00080
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• 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

Motivation

Retailers set prices and stock levels without knowing how demand responds to price. They must learn the demand curve from their own sales while still earning money, which is the exploration–exploitation trade-off of dynamic pricing with learning (den Boer 2015). Two features of practice make the problem harder than the textbook bandit. First, demand is censored: when the shelf runs empty, the firm sees only its sales $\min\{d_t,y_t\}$, not the demand $d_t$. Second, firms change prices rarely, because of menu costs and customer reaction, so a policy may change its price at most $m$ times over the whole horizon (Cheung, Simchi-Levi and Wang 2017).

Chen, Chao and Wang study a firm facing both features at once, in a parametric model where the demand distribution is known up to a parameter. For the well-separated case they give an algorithm, Algorithm-I, whose regret grows as $T^{1/(m+1)}$, and they show that no admissible policy does better in general. This mission formalizes the upper bound. A companion mission formalizes the lower bound.

Setting

A firm sells one product over periods $t=1,\dots,T$. At the start of period $t$ it holds inventory $x_t$ (with $x_1=0$). It chooses a price $p_t\in\mathcal P=[p^l,p^h]$ and an order-up-to level $y_t\in\mathcal Y=\{y^l,\dots,y^h\}$ with $y_t\ge x_t$, and the order arrives at once. Demand $d_t$ then has probability mass function $f(\cdot;p_t,z)$ on $\{d^l,d^l+1,\dots,d^h\}$, where $d^h\le+\infty$ and the parameter $z$ lies in $\mathcal Z=[z^l,z^h]$, $0\le z^l\le z^h$. Unmet demand is lost, and the firm observes only the sales $\min\{d_t,y_t\}$. Leftover stock carries over, $x_{t+1}=(y_t-d_t)^+$. Each unit left over costs $h\ge0$ and each lost sale costs $b\ge0$. The single-period expected profit is

$$G(p,y,z)=p\,\mathbb E[D(p,z)]-h\,\mathbb E[y-D(p,z)]^+-(b+p)\,\mathbb E[D(p,z)-y]^+ .$$

For each $y$, $p^*_y(z)$ is an optimal price, $\max_{p\in\mathcal P}G(p,y,z)=G(p^*_y(z),y,z)$, and the clairvoyant value is $G^*(z)=\max_{(p,y)\in\mathcal P\times\mathcal Y}G(p,y,z)$.

A policy's decision in period $t$ may depend only on past decisions and past sales. The regret of a policy is

$$R(T)=T\,G^*(z)-\mathbb E[V^\phi(T,z)]=\sum_{t=1}^T\mathbb E\big[G^*(z)-G(p_t,y_t,z)\big].$$

The family is well-separated (Definition 1) if for every price the pmfs $f(\cdot;p,z)$, $z\in\mathcal Z$, are pairwise distinct.

Algorithm-I splits the horizon into $m+1$ stages of lengths $I_i=\lceil T^{i/(m+1)}\rceil$ for $i\le m$, with $I_{m+1}=T-\sum_{i\le m}I_i$. Stage $i$ uses one price $\hat p_i$ and the order-up-to target $\tilde y_i$. The target equals the planned level $\hat y_i$, raised by $\Delta\ge1$ when $\hat y_i=d^l$ so that the sales carry information. At the end of the stage the algorithm computes the censored-data maximum-likelihood estimate $\hat z_i$ (5). It then sets the next stage's decisions to a maximizer of $G(\cdot,\cdot,\hat z_i)$ (6). It changes its price at most $m$ times.

Formalization targets

Goal: Theorem 1

Under Assumption A (regularity of $G$ and of $p^*_y$ near the true $z$), Assumption 1 (Fisher-information bounds, a positive lower bound on the pmf, strict monotonicity of $f(d^l;p,\cdot)$), Definition 1, and the condition that every optimal order-up-to level exceeds $d^l$, there is $K_6>0$ such that for all large $T$

$$R(T)\le K_6\,T^{\frac1{m+1}} .$$

The constant may depend on the model, the true parameter and the algorithm's inputs. The rate $T^{1/(m+1)}$ is the content.

Milestones

1. Theorem B1: if an estimator satisfies $\mathbb P\{\|\hat z-z\|\ge\epsilon\}\le K_{14}e^{-nK_{15}\epsilon^2}+K_{16}/n$, then the plug-in decision has optimality gap $G^*(z)-\mathbb E[G(\hat p^*,\hat y^*,z)]\le K_{17}/n$.
2. Proposition 1: the censored MLE satisfies $\mathbb P\{|z-\hat z_i|\ge\epsilon\}\le K_3e^{-K_4I_i\epsilon^2}+K_5/I_i$.
3. Per-stage estimation regret (p. 25): $\mathbb E[G^*(z)-G(\hat p_i,\hat y_i,z)]\le K_{17}/I_{i-1}$.
4. (25): the summed estimation regret is at most a constant times $mT^{1/(m+1)}$.
5. (26): $\mathbb P(\hat y_i\ne\tilde y_i)\le K/I_{i-1}$, so exploration after stage 1 is rare.

Significance

The upper bound shows that a budget of $m$ price changes costs only a $T^{1/(m+1)}$ regret even under censoring. With $m$ of order $\log T$ the rate drops to logarithmic (Theorem 3 of the paper). Together with the matching lower bound (Theorem 2), it identifies the exact price of limiting price changes in this model. Theorem B1 is a general transfer principle, from a large-deviation bound on an estimate to a $1/n$ optimality gap of the plug-in decision. It allows continuous and discrete decisions together and needs no unique optimizer. It is reusable for any parametric learning problem with that structure. Proposition 1 is a large-deviation bound for maximum likelihood from censored, dependent, non-identically distributed data. The paper notes that such results were not previously available in the statistics literature.

The results are proved in the paper's appendices. None of them has a machine-checked proof. A formalization would check the regret decomposition (23), the stagewise bookkeeping with ceilings, and the large-deviation argument for the censored MLE. It would also make the reading of several loosely stated steps exact (see Formalization scope).

Difficulty

The obvious argument plugs a consistent estimator into the optimizer and bounds the regret by the estimation error. It fails twice. The error of $\hat z_i$ is of order $I_{i-1}^{-1/2}$, so a Lipschitz bound on the profit would give regret of order $I_i/\sqrt{I_{i-1}}$ per stage, which is too large. The $1/n$ rate of Theorem B1 needs the first-order condition at an interior optimum and the exact gap $\delta$ between optimal and suboptimal discrete levels. Second, the data are censored and dependent. The censoring level $y_t$ depends on carried inventory, which depends on past demand and on past prices. The classical large-deviation results for maximum likelihood assume i.i.d. uncensored samples (Borovkov 1998) and do not apply. Proposition 1 needs a separate argument that the inventory target is reached in most periods with high probability.

Formalization scope

The model is encoded with a scalar parameter. $\mathcal P$, $\mathcal Y$ and $\mathcal Z$ are as above. The pmf is positive exactly on $\{d^l,\dots,d^h\}$ and sums to one, and $d^h=+\infty$ is allowed. The expected profit $G$ is built from these sums. $G^*(z)$ is the finite maximum $\max_{y}G(p^*_y(z),y,z)$ for a price selection $p^*$, not a real supremum. Periods are 0-based in Lean, while stages keep the paper's indices. Expectations and probabilities are sums over demand paths $d\in\mathbb N^T$ weighted by $\prod_tf(d_t;p_t,z)$, the law of the path under the algorithm, taken in $[0,\infty]$. Every regret summand is nonnegative.

Algorithm-I reads demand only through sales. Step 2's arg max is any maximizer of the censored product likelihood, which exists by compactness. Step 3's arg max is $\hat y$, any maximizer of $y\mapsto G(p^*_y(\hat z),y,\hat z)$, together with the price $p^*_{\hat y}(\hat z)$ of Assumption A(iii). This is the decision the proof of Theorem B1 analyses. Proposition 1's "large enough $i$" is read as "large enough $T$, uniformly in the stage and in $\epsilon$". Theorem B1 is stated for a scalar price and level and a parameter in $\mathbb R^k$.

Three hypotheses are added and disclosed. Differentiability of $f$ in $z$ is presupposed by Assumption 1. Finiteness of the mean demand is needed for (4) when $d^h=\infty$. The condition $d^l\le y^l$ is needed because Step 1 defines the target only for $\hat y\ge d^l$. "The optimal order-up-to level exceeds $d^l$" is read for every optimal level.

A trivializing formalization is ruled out. Regret and probabilities are path sums of nonnegative terms, not Bochner integrals that vanish on non-integrable inputs. $T^{1/(m+1)}$ is a real power. The hypotheses are jointly satisfiable: a Bernoulli instance with $\mathcal Y=\{1\}$, $\mathcal P=[1,2]$, $\mathcal Z=[2/3,4/5]$, $f(0;p,z)=zp/2$ satisfies all of them, together with explicit selections, and this has been verified in Lean.

A complete development needs the following:

• Hoeffding-type concentration for dependent bounded sums;
• a large-deviation bound for the censored log-likelihood;
• Taylor's theorem with integral remainder on an interval;
• bookkeeping lemmas for the stage lengths $\lceil T^{i/(m+1)}\rceil$.

Theorem B1 and the model definitions are reusable for the paper's later results (Theorems 3, 5, 6), which repeat these arguments. Contributions to any milestone are welcome, including alternative proofs of Proposition 1.

Selected references

• B. Chen, X. Chao, Y. Wang, Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, Operations Research (technical note), 2020; read in the SSRN revision of 2020-02-10. https://doi.org/10.1287/opre.2020.1993, https://ssrn.com/abstract=2700747
• W. C. Cheung, D. Simchi-Levi, H. Wang, Dynamic Pricing and Demand Learning with Limited Price Experimentation, Operations Research 65(6), 2017. https://doi.org/10.1287/opre.2017.1629
• J. Broder, P. Rusmevichientong, Dynamic Pricing under a General Parametric Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1057
• A. A. Borovkov, Mathematical Statistics, Gordon and Breach, 1998.
• A. V. den Boer, Dynamic pricing and learning: Historical origins, current research, and new directions, Surveys in Operations Research and Management Science 20(1), 2015. https://doi.org/10.1016/j.sorms.2015.03.001

Motivation

A seller with a fixed stock must choose prices before knowing when customers will arrive or what they will be willing to pay. If customers can wait for a later price, the seller must also account for how today's price changes their purchasing decisions. Chen and Farias study this problem with strategic customers and identify a simple inventory-based policy that can be compared with the best attainable revenue. Their Theorem 1 shows that this policy, with discount rate $\beta=1/(1.42T)$ for a season of length $T$, earns at least $0.29$ of the optimal expected revenue. The policy posts the price that is optimal in the canonical discounted revenue-management problem with myopic customers (Gallego and van Ryzin, 1994; Farias and Van Roy, 2010) at the current inventory level. This mission targets the lower-bound half of its argument, stated as Lemma 9: a comparison between the policy's revenue over a fixed selling season and a discounted, infinite-horizon value. The latter comparison is meaningful independently of the paper's strategic-customer benchmark.

Setting

The seller begins with inventory $x_0\in\mathbb N$ and sells at most one item to each customer. Customers arrive at rate $\lambda>0$. Their nonnegative valuations have density $f$ with total mass one. Write $\bar F(p)=\int_p^\infty f(v)\,dv$ for the probability that a valuation exceeds price $p$. A customer who behaves myopically buys at a posted price $p$ exactly when the valuation is high enough, so sales occur at rate $\lambda\bar F(p)$ while that price is posted.

The paper's Assumption 1 concerns the virtual value $\psi(p)=p-\bar F(p)/f(p)$: it is nondecreasing on nonnegative prices and has a nonnegative root. The simple policy is built from a discount rate $\beta>0$ and an infinite-horizon Bellman value $V:\mathbb N\to\mathbb R$. It has $V(0)=0$ and, for $x\ge1$, satisfies the sign-corrected recursion

$$\beta V(x)=\sup_{p\ge0}\lambda\bar F(p)\bigl(p+V(x-1)-V(x)\bigr).$$

At inventory $x\ge1$ the root price $\pi(x)$ is the unique nonnegative solution of $\psi(\pi(x))=V(x)-V(x-1)$. The price posted just before a sale is $\pi(x)$, and the inventory then becomes $x-1$. At zero inventory the posted price is infinity and there are no more sales. The expected sum of prices paid at sales by time $T$ is denoted $J(x_0,T)$. These objects come from §§2–3.1 of the paper.

Formalization targets

The goal is Lemma 9, for every $\lambda,\beta,T>0$ and every initial inventory $x_0$:

$$V(x_0)\le\left(1+\frac{e^{-\beta T}}{\beta T}\right)J(x_0,T).$$

The coefficient is part of the target. No choice of $\beta$ is fixed. The milestones follow the results stated in the paper: inventory monotonicity of $V$, price monotonicity, pathwise monotonicity of the price and its revenue rate (Lemma 7), the expected-rate identity, revenue-per-time monotonicity (Lemma 8), the identification of $V$ with discounted policy revenue, and the comparison through an independent exponential horizon. The last milestone evaluates $\mathbb E[\max\{1,X/T\}]$ exactly for $X\sim\operatorname{Exp}(\beta)$.

Significance

The bound quantifies how much of the discounted value this explicit policy earns within a finite selling season. Its factor depends only on the dimensionless product $\beta T$; it does not depend on inventory, arrival rate or valuation density. Together with the paper's separate upper bound on its strategic benchmark, Lemma 9 contributes to the advertised $0.29$ comparison. The full comparison requires definitions and equilibrium arguments beyond this mission, so the goal here is precisely the fixed-horizon lower bound.

Chen and Farias proved these statements in the published paper. The Lean items in this proposal are statements awaiting machine-checked proofs. A completed development would establish the discounted-value verification step and the fixed-horizon comparison for an explicit pure-death sales process. Its constructions of inventory-dependent sale times and finite-horizon revenue could also be reused in other pricing models with Poisson arrivals.

Difficulty

The Bellman value is specified by an optimization equation, while $J(x_0,T)$ is defined from the actual sales process. Their equality at an exponential horizon does not follow by unfolding a definition. The price chosen through the virtual-value equation must be connected to the Bellman optimum, and the inventory-dependent process must be related to the same value. The paper also relies on the fact that the root price falls as inventory rises, citing Lemma 1 of Farias and Van Roy; that fact does not follow merely from monotonicity of $\psi$ without control of the marginal values $V(x)-V(x-1)$. Lemma 8 then concerns expected revenue over two different horizons, including paths that sell out early.

Formalization scope

The Lean model uses a nonnegative integrable density on $\mathbb R$, zero on negative valuations and normalized to mass one. It adds $f(p)>0$ for every $p\ge0$. This disclosed condition excludes bounded-support densities: without it the paper's quotient $\bar F(p)/f(p)$ can divide by zero and Lean would assign a spurious value. The paper says the root equation has a unique solution under Assumption 1, but nondecreasing $\psi$ alone does not guarantee existence or uniqueness. Accordingly, the root policy is characterized by its equation and an explicit uniqueness condition. The Bellman recursion uses a least-upper-bound predicate rather than a real supremum with a default value on an empty or unbounded set. The corrected sign in the recursion matches the paper's root equation and discounted-revenue equation.

For stock $x_0$, the model uses $x_0$ independent rate-one exponential clocks. At inventory $x$, the next holding time is the next clock divided by $\lambda\bar F(\pi(x))$. Sales are numbered $1,\ldots,x_0$, and sale $k$ earns $\pi(x_0-k+1)$. The law is the myopic sales process with intensity $\lambda\bar F(\pi(x))$. Expected revenues are lower integrals in the extended nonnegative reals; nonnegative prices make their real-to-extended conversion exact. An independent $X\sim\operatorname{Exp}(\beta)$ is represented by an outer integral over its law. The factor $\lambda$ missing from the paper's printed compensator display is restored, and the paper's intermediate $1+e^{-\beta T}/T$ is read with the missing $\beta$ restored.

The strategic-customer types, stopping rules, perfect Bayesian equilibrium, and the identification of the strategic policy's revenue with myopic-sales revenue are not formalized here. Neither are Theorem 1's $\mathrm{OPT}$ and $J^*$ benchmarks: their specification is not pinned down sufficiently in the paper for this proposal. In particular, $J$ is constructed from sale times and payments, never from $V$, and $V$ is specified by the Bellman equation, never as the policy's revenue. Contributions toward the goal include the individual milestones and reusable facts about the clock process, its revenue, and the exponential horizon.

Selected references

• Y. Chen and V. F. Farias, Robust Dynamic Pricing with Strategic Customers, Mathematics of Operations Research 43(4):1119–1142, 2018. DOI: 10.1287/moor.2017.0897.
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. DOI: 10.1287/mnsc.40.8.999.
• V. F. Farias and B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010. DOI: 10.1287/opre.1090.0729.
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. DOI: 10.1007/978-1-4684-9477-8.