Operations Research

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

A partially observable Markov decision process (POMDP) models a controller that cannot see the state of the system it steers, only noisy observations of it. Inventory control with unrecorded demand, machine maintenance with imperfect inspection, and target tracking from sensor readings all have this form. The standard way to solve a POMDP is to replace it by its belief MDP, also called the completely observable MDP (COMDP): the state becomes the posterior distribution of the hidden state given everything observed so far. The belief MDP is fully observed, so the theory of Markov decision processes applies to it, but only if the belief MDP satisfies that theory's hypotheses. For MDPs with Borel state and action spaces, unbounded costs and possibly noncompact action sets, the hypothesis that yields optimality equations, convergence of value iterations and stationary optimal policies is Assumption (W*) of Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 2012): the cost is $\mathbb K$-inf-compact and the transition probability is weakly continuous.

Before Feinberg, Kasyanov and Zgurovsky (arXiv:1401.2168v2, published in Math. Oper. Res. 41(2), 2016), sufficient conditions for the belief MDP to be weakly continuous required a weakly continuous filter (Hernández-Lerma, 1989, as recalled on p. 11 of arXiv:1401.2168v2), a condition that fails in many natural models. The paper replaces it by a condition on the primitive data of the POMDP.

Setting

Let $\mathbb X$ (states), $\mathbb Y$ (observations) and $\mathbb A$ (actions) be Borel subsets of Polish spaces. Let $P(dx' \mid x, a)$ be the transition kernel on $\mathbb X$ given $\mathbb X \times \mathbb A$, $Q(dy \mid a, x)$ the observation kernel on $\mathbb Y$ given $\mathbb A \times \mathbb X$, and $c : \mathbb X \times \mathbb A \to \mathbb R \cup \{+\infty\}$ a Borel one-step cost bounded below. $\mathbb P(\mathbb X)$ is the set of probability measures on $\mathbb X$ with the topology of weak convergence ($\int f\,d\mu_n \to \int f\,d\mu$ for bounded continuous $f$). A sequence $\mu_n$ converges setwise if $\mu_n(C) \to \mu(C)$ for every Borel $C$, and in the total variation if $\sup_f |\int f\,d\mu_n - \int f\,d\mu| \to 0$ over Borel $f$ with values in $[-1, 1]$. A kernel is weakly (setwise, total-variation) continuous if $x_n \to x$ implies the corresponding convergence of the measures.

For a belief $z \in \mathbb P(\mathbb X)$ and an action $a$, let $R(B \times C \mid z, a) = \int_{\mathbb X} \int_B Q(C \mid a, x')\,P(dx' \mid x, a)\,z(dx)$ be the joint law of the next state and observation (3.1), and $R'(C \mid z, a) = R(\mathbb X \times C \mid z, a)$ its observation marginal (3.2). A filter is a kernel $H(dx \mid z, a, y)$ with $R(B \times C \mid z, a) = \int_C H(B \mid z, a, y)\,R'(dy \mid z, a)$ (3.3): $H(z, a, y)$ is the posterior after observing $y$. The belief MDP has state space $\mathbb P(\mathbb X)$, action set $\mathbb A$, cost $\bar c(z, a) = \int c(x, a)\,z(dx)$ (3.8), and transition $q(\cdot \mid z, a)$, the law of $H(z, a, y)$ when $y \sim R'(\cdot \mid z, a)$ (3.5). A cost is $\mathbb K$-inf-compact on $\mathbb S_1 \times \mathbb S_2$ if its restriction to $K \times \mathbb S_2$ has compact level sets for every compact $K \subseteq \mathbb S_1$.

Formalization targets

Goal: Theorem 3.6

If either Assumption (D) ($0 \le \alpha < 1$) or Assumption (P) ($c \ge 0$ and $0 \le \alpha \le 1$) holds, $c$ is bounded below and $\mathbb K$-inf-compact on $\mathbb X \times \mathbb A$, $P$ is weakly continuous and $Q$ is continuous in the total variation, then the belief MDP satisfies Assumption (W*):

$$\bar c \text{ is bounded below and } \mathbb K\text{-inf-compact on } \mathbb P(\mathbb X) \times \mathbb A, \qquad (z_n, a_n) \to (z, a) \implies q(\cdot \mid z_n, a_n) \to q(\cdot \mid z, a) \text{ weakly}.$$

The two halves

• Cost half (Theorem 3.4, through Lemma 6.1 and Lemma 5.1(ii)): $\bar c$ is bounded below by the same constant as $c$ and $\mathbb K$-inf-compact.
• Transition half (Theorem 3.7): under the hypotheses on $P$ and $Q$, $R'$ is setwise continuous and Assumption (H) holds: whenever $z_n \to z$ and $a_n \to a$, along a subsequence $H(z_{n_k}, a_{n_k}, y) \to H(z, a, y)$ weakly for $R'(\cdot \mid z, a)$-almost every $y$. Theorem 3.5 then gives weak continuity of $q$. The route runs through Theorem 5.2, Lemma 5.3, Corollary 5.4, Theorem 5.5 and Lemma 5.6.

Significance

Theorem 3.6 supplies the hypothesis under which the cited general MDP theory gives stationary optimal policies, optimality equations and convergence of value iterations for total-cost POMDPs in terms of $P$, $Q$ and $c$ alone, without compactness of the action set, boundedness of the cost or continuity of the filter. It covers, for example, observation kernels with densities continuous in $(a, x)$, and the paper applies it to inventory control with incomplete records and to the Kalman filter. Example 4.1 of the same paper shows that total-variation continuity of $Q$ cannot be weakened to setwise continuity.

The result is proved in the paper; this proposal poses its formal statement and the supporting results as proof targets. Completing them would provide a checked bridge from POMDPs to the general MDP theory under weak continuity, together with reusable facts about weak, setwise and total-variation convergence: equicontinuity of integrals against weakly continuous kernels (Theorem 5.2), the convergence-in-probability criterion (Theorem 5.5), and the generalized Fatou lemmas.

Difficulty

The posterior $H(z, a, y)$ is defined only for $R'(\cdot \mid z, a)$-almost every $y$ and has no continuous version in general, so weak continuity of $q$ cannot be read off from continuity of $H$. The tempting argument, that continuous $P$ and $Q$ make the Bayes posterior move continuously, fails: $\mathbb Y$ need not be countable and $Q$ need not have densities. What has to be controlled is the joint law $R$ on sets $(\mathcal O_1 \setminus \mathcal O_2) \times C$ uniformly in the observation set $C$; convergence for each fixed $C$ is not enough. Turning this uniform control into almost-sure convergence of posteriors along a subsequence requires a diagonal argument over a countable base of $\mathbb X$. On the cost side, the difficulty is that $c$ may take the value $+\infty$ and is not continuous; $\mathbb K$-inf-compactness has to be transported through integration against a weakly converging sequence of measures.

Formalization scope

All definitions live in FeinbergPOMDP.WStar.Model. $\mathbb X, \mathbb Y, \mathbb A$ are separable metrizable spaces with their Borel σ-algebras (PolishSpace is not assumed, since Borel subsets of Polish spaces need not be Polish); $\mathbb X$ is additionally nonempty and standard Borel in Theorems 3.6 and 3.7, where a filter must exist. $\mathbb P(\mathbb X)$ is Mathlib's ProbabilityMeasure with the weak topology. All continuity notions are the paper's sequential ones; total variation is the supremum over Borel functions with values in $[-1, 1]$, written in $\varepsilon$–$N$ form, while the set-indexed suprema of (5.15) and (5.17) keep their set form. The cost is written $c = \ell + f$ with $\ell \in \mathbb R$ and $f$ taking values in $[0, \infty]$, so $\bar c = \ell + \int f\,dz$, exact even when $c = +\infty$ on a set of positive measure. $\mathbb K$-inf-compactness is the published FeinbergLiang.ACOE.KInfCompact. A filter is a map $H : \mathbb P(\mathbb X) \to \mathbb A \to \mathbb Y \to \mathbb P(\mathbb X)$ that satisfies (3.3) and is jointly Borel measurable in $(z,a,y)$, as the paper's stochastic kernel is; $q$ is the image of $R'$ under $H(z, a, \cdot)$ for the Borel σ-algebra of the weak topology on $\mathbb P(\mathbb X)$.

Since $q$ does not depend on the choice of filter, every statement about $q$ is made for every filter satisfying (3.3). A fixed filter that ignores the observation, such as $H(z, a, y) = z$, would make $q$ a point mass and the weak continuity trivial; it satisfies (3.3) only when observations carry no information, and is excluded by quantifying over all filters.

The goal states the Assumption (W*) conclusion of Theorem 3.6. Its tail, "statements (i)–(vi) of Theorem 3.1 hold", invokes Theorem 2.1 of Feinberg et al. (2012) applied to the belief MDP; it is cited rather than proved in this paper. Generalized Fatou's lemmas 5.1(i) and 5.1(ii) are referenced from the published Schäl (1993) items. A complete development needs weak and setwise convergence on ProbabilityMeasure, portmanteau-type arguments, disintegration (Measure.condKernel) and the identification of the Borel and Giry σ-algebras on $\mathbb P(\mathbb X)$; the last is missing from Mathlib and is a welcome contribution in its own right. Proofs of any milestone, and alternative arguments for Theorem 3.7, are welcome.

Selected references

• E. A. Feinberg, P. O. Kasyanov, M. Z. Zgurovsky, Partially Observable Total-Cost Markov Decision Processes with Weakly Continuous Transition Probabilities, arXiv:1401.2168v2 (2014); Mathematics of Operations Research 41(2), 2016. https://arxiv.org/abs/1401.2168v2
• E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average-cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 2012. https://doi.org/10.1287/moor.1120.0555
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html
• M. Schäl, Average optimality in dynamic programming with general state space, Mathematics of Operations Research 18(1), 1993. https://doi.org/10.1287/moor.18.1.163

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

Distributionally robust optimization (DRO) evaluates a decision against a collection of probability distributions near an empirical one. In a finite scenario model, the familiar construction puts a divergence ball around the histogram of observed scenarios. Lam's empirical construction instead gives one weight to each observation, even when several observations have the same value. The distinction matters because a sample can contain repeated values and can omit some points of the stated support. The paper uses a Burg-entropy ball on those observation weights to recover statistical guarantees for an expected loss, despite the empirical ball having low probability of containing the true distribution. Lam, §§2.1–2.3, pp. 5–9.

Proposition 1 identifies what this observation-level construction becomes when the random quantity has finite support: its lower and upper DRO values coincide with values from a Burg-divergence ball on the support histogram. This links a method defined on individual data points to the standard finite-scenario formulation. The radius uses a one-degree-of-freedom chi-square quantile because the paper calibrates an expected value at a fixed decision; it does not use the $k-1$ degrees of freedom associated with estimating a full $k$-point distribution. Lam, Proposition 1, p. 11, and the discussion on pp. 8–9.

Setting

Fix a decision $x$ and a real loss $h(x;s_i)$ at each of $k$ support points $s_1,\ldots,s_k$. A sample of size $n$ has an assignment $c(j)$ telling which support point produced observation $j$. Write $n_i$ for the number of assignments to point $i$ and $\hat p_i=n_i/n$ for the empirical histogram. The support points need not all appear in the sample. The decision and loss only determine a finite vector of loss values; no probability space is needed for this deterministic comparison. Lam, §2.1, p. 6, and Proposition 1, p. 11.

The empirical Burg ball $\mathcal U_n(\eta)$ consists of observation weights $w_1,\ldots,w_n$ that are nonnegative, sum to one, and obey $-n^{-1}\sum_j\log(nw_j)\le\eta$. The support Burg ball $\mathcal U'_{\mathrm{Burg}}(\eta)$ consists of support weights $p_1,\ldots,p_k$ that are nonnegative, sum to one, are absolutely continuous with respect to $\hat p$, and obey $-\sum_i\hat p_i\log(p_i/\hat p_i)\le\eta$. At an observed point, finite Burg divergence requires $p_i>0$; at an unobserved point, absolute continuity requires $p_i=0$. Lam, (13)–(15), pp. 5–6; (19), p. 8; (28), p. 11.

For a support weight vector $p$, the expected loss is $\sum_i p_i h(x;s_i)$. For an observation weight vector $w$, it is $\sum_j w_j h(x;s_{c(j)})$. The empirical lower and upper values are the minimum and maximum over $\mathcal U_n(\eta)$; the support values use $\mathcal U'_{\mathrm{Burg}}(\eta)$. The same empirical ball is used for both bounds. Lam, (26)–(28), p. 11.

Formalization targets

The goal is Proposition 1. For every $n>0$, every assignment of the sample to finite support points, every fixed decision $x$, and every $\kappa\ge0$, set $\eta=\kappa/(2n)$. Then

$$\min_{w\in\mathcal U_n(\eta)}\sum_{j=1}^n w_jh(x;s_{c(j)}) =\min_{p\in\mathcal U'_{\mathrm{Burg}}(\eta)}\sum_{i=1}^k p_ih(x;s_i),$$ $$\max_{w\in\mathcal U_n(\eta)}\sum_{j=1}^n w_jh(x;s_{c(j)}) =\max_{p\in\mathcal U'_{\mathrm{Burg}}(\eta)}\sum_{i=1}^k p_ih(x;s_i).$$

The printed proposition takes $\kappa=\chi^2_{1,1-\alpha}$. The deterministic identity holds at every nonnegative $\kappa$, including zero. The two milestones record the source proof's statements that a feasible support vector gives a feasible observation vector with the same objective value, and conversely that a feasible observation vector gives a feasible support vector with the same objective value. Lam, Proposition 1, p. 11, proof p. 24.

Significance

The identity lets a finite-support user compute the empirical DRO values with one variable per distinct support point instead of one per observation, without changing either bound. It also shows precisely how Lam's empirical calibration relates to a conventional histogram-based divergence model: the ambiguity sets have different coordinates, but the resulting extrema of any loss constant on each class agree. This is the finite-support interpretation stated immediately after Theorem 2, and it explains the radius comparison on pp. 8–9. Lam, pp. 8–9 and Proposition 1, p. 11.

The result is proved in the paper; the remaining task is a machine-checked proof of the two transformations and the equality of extrema. The published formal library already contains the observation-level $\phi$-divergence ball and its robust upper mean, and a shared setting supplies the Burg generator and lower empirical value. This mission adds the support histogram, its Burg ball, and the bridge between the two representations. Those definitions and transformations can also be reused for other finite-support losses. The paper's separate pointwise coverage and consistency results are goals of other missions in this series. Lam, Theorems 2–3 and Proposition 1, pp. 11–12.

Difficulty

Repeated observations make the two weight spaces different: the empirical problem has $n$ coordinates and the support problem has $k$. Simply identifying coordinates loses multiplicities in both the normalization and the logarithmic divergence. Empty classes create a second boundary case, since no observation weight can be assigned to an unobserved support point. A statement that silently permits such mass changes the support optimization value. The full reduction must preserve feasible objective values in both directions, for the lower and upper extrema. Lam, proof of Proposition 1, p. 24.

Formalization scope

Lean uses Fin n for observations and Fin k for support points, with zero-based indices, a class map $c$, real loss values, and the paper's Burg generator valued in EReal. Nonpositive likelihood ratios receive $+\infty$. The empirical ball reuses the published PhiDivRobust.Counterpart.probUncertaintySet; its upper value is the published GenEmpLik.Expansion.robustMean. The lower value is a real infimum over the same ball. The condition $n>0$ and the nonnegative radius make both feasible value sets nonempty and bounded, so the real infimum and supremum mean the paper's minimum and maximum. The histogram can have zero entries. Lam, (19), (26)–(28), pp. 8, 11.

Display (28) omits a condition from the preceding definition of a divergence ball: $p$ must be absolutely continuous with respect to $\hat p$. Without it, an unobserved support point can receive positive mass and Proposition 1 is false. The formal support ball includes $\hat p_i=0\Rightarrow p_i=0$ from (13)–(14). It also requires $p_i>0$ where $\hat p_i>0$, because Lean's real logarithm returns zero at zero whereas the paper's Burg divergence is infinite there. These conditions, together with $n>0$, exclude trivial values from empty balls, division by zero, and logarithms at invalid weights. The decision set $\Theta$ is omitted because the paper fixes one $x$ and the result holds for every such $x$. Lam, (13)–(14), pp. 5–6, and (28), p. 11.

The development needs finite-sum identities, elementary properties of the probability simplex, the logarithm's concavity, and bounds on the extrema of bounded nonempty finite-dimensional value sets. Contributions that establish the two direction statements, or reusable facts about aggregation of finite probability weights, directly advance this mission. The paper's uniform calibration theorem, Theorem 4, is outside this scope: it needs a Donsker class, a data-dependent chi-square process, and its supremum quantile, none of which enters Proposition 1. Lam, Theorem 4, pp. 13–14.

Selected references

• Henry Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; published in Operations Research 67(4), 2019. arXiv, DOI.

Why limited price changes matter

A seller learning a demand curve normally adjusts prices as new observations arrive. A price-change limit prevents that continual adjustment: a price may have to be chosen before the seller knows which demand curve it faces, then held through a block of sales. This matters when repricing is operationally costly, constrained by contracts, or visible to customers. Chen, Chao and Wang study pricing jointly with inventory replenishment under censored demand. Their Theorem 2 asks how much regret is unavoidable when the seller can change price at most $m$ times, regardless of the learning policy it uses (SSRN revision, pp. 10–11, 35–42).

The lower bound is paired with their Theorem 1: in the well-separated setting an algorithm attains regret proportional to $T^{1/(m+1)}$ for large horizons, while Theorem 2 asserts the same exponent cannot be improved uniformly over admissible policies (SSRN revision, p. 10). The paper appeared as an Operations Research technical note in 2020 (DOI 10.1287/opre.2020.1993); this mission cites the authors' SSRN revision dated 2020-02-10, whose page and result numbers are used throughout.

Bernoulli pricing setting

The horizon has $T$ periods. At each period the seller posts a price $p_t\in[1,6]$ and replenishes inventory to one unit. Demand $d_t$ is either zero or one, so all demand can be served and the observed sale equals demand. The unknown scalar parameter $z$ belongs to $[1/6,5/6]$. Conditional on the posted price, the probability of one unit of demand is

$$\nu(p,z)=\max\{0,1-pz/2\}.$$

Holding and shortage costs are zero. Hence expected one-period revenue is $r_z(p)=p\nu(p,z)$. The clairvoyant benchmark is $G^*(z)=1/(2z)$: it is attained by the feasible price $p^*=1/z$. The local Lean sanity check proves this maximum property, so the benchmark does not rely on a default value of a supremum. The model is the explicit Bernoulli construction in the proof of Theorem 2 (SSRN revision, p. 35).

An admissible randomized policy may draw random bits and use past posted prices and observed sales when choosing its next price. Its action cannot depend on future demand or on the unknown parameter. Every realized seed and demand path must satisfy the price-change constraint

$$\sum_{t=1}^{T-1}\mathbf 1\{p_t\ne p_{t+1}\}\le m,\qquad m\ge1.$$

The regret $R_\pi(T,z)$ is the expected sum of $G^*(z)-r_z(p_t)$ under the policy and the demand law at parameter $z$. The paper's admissibility and change constraint are stated on pp. 5–6; its randomized policy factorization is displayed in (49) on p. 35 (SSRN revision).

Formalization targets

The goal is the minimax reading of Theorem 2. For each fixed $m\ge1$, there is a positive constant $K_7$ and a horizon threshold $T_0$, independent of the policy and the horizon, such that

$$\forall T\ge T_0\;\forall\pi\text{ admissible with at most }m\text{ changes},\quad \exists z\in[1/6,5/6]:\ R_\pi(T,z)\ge K_7T^{1/(m+1)}.$$

The parameter is selected after the policy. The proof's objective (56) is a worst-case parameter choice for each policy (SSRN revision, p. 37). The printed theorem sentence can also be read as one fixed instance defeating every algorithm; that order is false because a policy supplied with that instance's $z$ can post $1/z$ in every period.

Five milestones expose the source's quantitative ingredients. The hierarchy (50) constructs parameters $z_\zeta$ from signs $\zeta\in\{\pm1\}^{m+1}$ and scales $\varepsilon_\ell=T^{-\ell/[2(m+1)]}$. Its parameters lie in $[1/6,5/6]$ for large $T$. Different signs are separated at scale $\varepsilon_\ell/8$. Lemma 1 bounds one-period regret by the squared error in a nearest-instance selection. The pointwise inequality underlying (57) gives a cost of at least $10^{-4}\varepsilon_\ell^2$ for a wrong sign. A corrected Lemma 2 supplies a quadratic Bernoulli relative-entropy bound under an explicit interior condition (SSRN revision, pp. 36–37).

What the result establishes

The exponent $1/(m+1)$ quantifies the cost of the change budget: fixing $m$ leaves a polynomial regret floor even though the Bernoulli demand law is one-dimensional and observed without censoring. Since the constructed instance fixes inventory at a level that serves every demand, a lower bound here also applies to policies in the joint pricing and inventory setting whenever that instance is admitted. It identifies the information loss caused by limited repricing, independently of lost sales and censoring.

The paper states the lower bound and gives a proof, but its printed Lemma 2 is false at prices where $\nu(p,z)=0$. The subsequent Lemma 3 applies that unrestricted bound. Therefore the source proof does not, as printed, establish the minimax claim for every admissible price policy. The Lean goal is an open target; the four elementary milestones and corrected information bound are also open Lean statements. Formalizing this mission requires an argument that handles prices at the zero-demand kink, or a different route to the lower bound. No machine-checked proof of this specific result is claimed here.

Where the argument is difficult

The natural comparison of two nearby parameters uses the relative entropy between their observed demand laws. Away from the kink, this information is quadratic in the parameter difference. At a price that makes demand impossible under one parameter but possible under the other, the divergence in the printed direction can be linear in that difference. The unrestricted $108|z-z'|^2$ bound of Lemma 2 therefore fails at exactly the prices an arbitrary policy may choose. Restricting the policy's prices would change the target. A faithful proof must retain those prices while still controlling the policy's information and regret (SSRN revision, Lemmas 2–3, pp. 36–40).

Formalization scope

Lean represents the horizon by Fin T; its index zero is period one in the paper. Bernoulli demand paths have type Fin T → Bool. A policy's price at a period depends on a random seed and only the earlier demand bits; with inventory level one, these bits are exactly the observed sales. A probability measure on the seed models adaptive randomization, including a pre-sampled stream of random choices. Prices are measurable functions of the seed for each finite history. The budget holds on every seed and path, not only on average.

Path probabilities are finite products of conditional Bernoulli probabilities. Regret is a finite sum of nonnegative gaps integrated over the seed with lintegral, so it cannot become zero through non-integrability of a real-valued expectation. The exponent of $T$ and the scales $\varepsilon_\ell$ use real division. The arg-min in (51) is any genuine nearest-instance selection; a local proof checks that one exists. The hierarchy's validity and separation statements require a large-horizon threshold, which the unqualified printed prose omits. The corrected Lemma 2 adds $pz\le11/6$ to keep the Bernoulli probabilities in the interior. Its verbatim milestone retains the printed statement, and its formal statement and note disclose the correction. Lemma 3 is not stated because its printed proof relies on Lemma 2 outside that interior region.

The named Bernoulli family strengthens the theorem's existential instance wording, while also exposing a limitation: at $p\ge2/z$ it violates the positive-mean and identifiability conditions stated earlier in the paper. That discrepancy is recorded rather than hidden in an assumption. Definitions for randomized adapted policies, finite path laws, the parameter hierarchy, and Bernoulli relative entropy are reusable; contributions that establish the open goal or repair the information comparison are in scope.

Selected references

• B. Chen, X. Chao, and Y. Wang, Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, SSRN 2700747, revision of 2020-02-10. Preprint.
• B. Chen, X. Chao, and Y. Wang, Technical Note—Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, Operations Research, 2020. DOI 10.1287/opre.2020.1993.

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