All missions

Learning prices and inventory together

A retailer selling perishable products must choose both a selling price and an inventory position. The two decisions affect sales, spoilage, stock carried to the next period, and the information available for future decisions. Demand parameters may change during the selling horizon, while the distribution of demand disturbances and the distribution of perishability are initially unknown. The paper of Keskin, Li and Song proposes policies that combine price experimentation, statistical estimation, and change detection. This mission concerns its stated regret guarantees for both policies, including the intermediate results used in their analysis.

The stochastic inventory model

There are $T$ selling periods. A history policy chooses a real price $p_t$ and a real order-up-to level $y_t$ using past observed demands, perished proportions, and actions. Prices and inventory positions belong to nondegenerate compact intervals $P$ and $Y$ with positive endpoints. Replenishment has zero lead time and no fixed ordering charge. Unmet demand is lost but observed.

Demand is $D_t=g(\alpha_t+\beta_t p_t)+\varepsilon_t$. The known link $g$ is increasing and twice continuously differentiable. The unknown pair $\theta_t=(\alpha_t,\beta_t)$ lies in a compact rectangle with negative price coefficient. It has $C$ change points; distinct parameter values are separated by a positive distance. There is no minimum duration for a constant segment. The disturbances are independent and identically distributed, centered, and have a bounded second moment and a local moment generating function bound. Their distribution may have atoms. A separate independent sequence of perished proportions has a beta distribution with an unknown, time-independent parameter in a positive compact rectangle.

Inventory evolves according to $x_{t+1}=[(1-q_t)y_t-D_t]^+$. A feasible decision satisfies $y_t\ge x_t$. Known nonnegative holding, lost-sales, disposal, and ordering costs are denoted by $h,b,w,c$. The standing restriction is $|h-c|<b+p$ for every allowed price. The single-period expected profit $Q$ is defined by the actual cost integrals in equations (4)–(5), including perishability and both positive-part losses.

The full-information anticipatory benchmark, or FIA, knows the complete deterministic parameter sequence and the primitive laws, but cannot observe future shocks. It maximizes the expected total reward in equation (3), including terminal salvage. The paper explicitly assumes an interior optimal solution exists. Learner and benchmark have separate inventory trajectories on common primitive shocks. Their regret is the expectation of the signed sum of their single-period profit differences.

Formalization targets

The principal target is both clauses of Theorem 1 in the supplied paper:

$$\Delta_N(T)\le K_1 T^{2/3}\sqrt{\log T},\qquad \Delta_E(T)\le K_2\sqrt T\log T\quad(T=3,4,\ldots).$$

Each constant is positive, finite, and chosen before the horizon and the allowable locations and values of the changes. Constants may depend on the fixed change-count bound, model bounds, noise law, separation, and policy tuning. The learner's rules are chosen before the unknown noise law, change count, separation, and environment. The conclusion includes their executability; the theorem does not assume away failed constructions.

Both policies alternate experimentation and profit maximization. Their experimental lengths and cycle lengths are the printed ceiling formulas. Experimental observations support demand quasi-likelihood estimation, beta maximum likelihood estimation, and change detection. Demand estimation uses observations since the last detected change; perishability estimation uses all past experimental observations. DDPO-N optimizes a residual-based empirical profit on a sparse price grid. DDPO-E fits a known exponential family and optimizes its estimated profit over the full continuous price interval. Both then apply the printed inventory adjustment.

The eleven milestones are Proposition 1, comparing FIA with the full-information non-anticipatory policy; Propositions 2–3 on parameter estimation; Lemmas EC.2 and EC.1 on noise moments, sample-cost tails, and optimal inventory; Propositions 4–7 on the two profit proxies and the pricing and inventory decisions; Theorem 2 on estimation regret for both policies; and Proposition 8 on delayed detections and early false alarms for both policies. Every displayed clause and constant factor is retained.

What the formalization contributes

The claimed bounds distinguish the effect of learning a general disturbance distribution from learning a known exponential-family representation. Their shared benchmark includes inventory carryover and anticipation of changing demand. A complete verification would therefore address more than a static estimation problem or a stationary pricing policy.

This mission supplies concrete statistical objects, observable histories, inventory dynamics, estimator relations, and the actual regret sums. Definitions contain no unproved assertions. The theorem declarations are open statement drafts, not machine-checked proofs. Formalization also exposes source defects that require scrutiny. In particular, an admissible small horizon produces contradictory experimental prices, and the general maximum-likelihood result does not assume identifiability. The stated targets retain those defects so that a proof or a disproof addresses the source claim.

Where the difficulty lies

Estimation, reset times, and optimizer choices depend on the same observed data. Replacing the resulting sample indices by a fixed independent sample changes the problem. Arbitrary disturbance laws also prevent silently assuming density lower bounds, smooth quantile inverses, or uniformly positive link derivatives. The source's proof of pricing convergence contains a derivative-sign gap; no such derivative hypothesis is added to the statement.

Partial operations create a separate issue. A quasi-likelihood equation may lack a root, a likelihood may lack a maximizer, and an experimental inventory position may be infeasible. An arbitrary default action would define a different algorithm. The execution relation instead retains all prescribed equations and actual optimizer requirements.

Formalization scope and conventions

Prices and inventories remain continuous. Probability uses infinite independent primitive sequences, while actual rewards stop at $T$. The infinite sequence matters for the literal indexing formula in Lemma EC.2. General exponential families use an explicit dominating measure, permitting continuous and discrete distributions without imposing identifiability or a convex parameter set. Measurable optimizer selections retain ties. Expectations that appear in asserted guarantees carry integrability content, preventing a divergent integral from becoming Lean's default zero.

The probability bounds with random $M_t$ are read literally: the event probability is a scalar, and its displayed comparison with the random right side holds almost surely on the stated range. The reset times remain random inside the event. Noise-only probabilities integrate the noise sequence with the perishability sequence fixed, recomputing the history and estimates. The inventory lemma asserts existence of the level identified by both formulas, without adding uniqueness. It uses extended-real infima and suprema, preserving empty-sign-set failures. A concrete lower-bound optimum makes the strict-negative-derivative set empty even in a model with an interior FIA solution; this source counterexample is recorded alongside the other findings.

Equation (6) is read consistently with equations (1)–(2), retaining $g$. Proposition 8(b) uses the lower endpoint $n\widehat\tau_j^-+1$ appearing in the final decomposition. Both readings are declared per item and recorded as source findings. The source basis is published, but the supplied artifact is internally dated January 3, 2021 and contains SSRN footers; citations use its own pages, not invented journal pagination. Empirical extensions, age-dependent spoilage, censored-demand experiments, and externally cited lower bounds are outside this mission.

Selected references

• N. B. Keskin, Y. Li and J.-S. Song, Data-Driven Dynamic Pricing and Ordering with Perishable Inventory in a Changing Environment, Management Science, 2022. DOI. The supplied artifact contains the main text on PDF pages 1–32 and its electronic companion on PDF pages 33–54; the selected results occur on pages 12, 21–25, 33 and 40.

Continuous monitoring and the cost of waiting

An A/B experiment collects observations while a user decides whether the evidence is strong enough to act. A user may inspect the experiment repeatedly and stop when a result looks convincing. A test calibrated only for one sample size does not automatically retain its error guarantee under that behavior. A sequential test instead makes the stopping decision part of the statistical procedure. In the supplied Johari–Pekelis–Walsh preprint, the question goes beyond error control: how much sampling does a continuously monitored test require compared with every other test offering at least its power?

Different users can tolerate different delays. One may abandon an experiment after a modest number of observations; another may wait longer. The paper models these choices by a maximum sample count and a tolerated probability of false rejection. Its first-order efficiency claim concerns a single family of tests that can accommodate these choices without knowing them when the mixing distribution is selected. This mission addresses that claim, using the exact preprint version and theorem numbering stated below.

Observations, decisions, and mixtures

Let $X_1,X_2,\ldots$ be independent identically distributed real observations under each parameter law $P_\theta$. The natural parameter ranges over an arbitrary nonempty open interval $\Theta\subseteq\mathbb R$, and $\theta_0\in\Theta$ is the null. The alternatives are all other parameters in the interval. The source's exponential family has densities $f_\theta(x)=f_0(x)\exp(\theta x-\psi(\theta))$. The cumulant $\psi$ is twice differentiable, has strictly positive second derivative, and each observation law has finite fourth absolute moment. These are the standing assumptions of Section 5.2, page 18.

A decision rule consists of a positive integer stopping time $T$, possibly infinite, and a binary decision $\delta$. Decisions use only the observations available at stopping. Rejection means $\delta=1$; a test that never stops must not reject. The rule has no access to the unknown parameter or to independent randomization outside the observation filtration. Its Type I error is $P_{\theta_0}(\delta=1)$.

Fix a mixing distribution $H$ on $\Theta$ with continuous strictly positive density throughout the interval. For $S_n=n^{-1}\sum_{i=1}^nX_i$, define

$$\Lambda_n^H=\int_\Theta \exp\{n[(\theta-\theta_0)S_n-(\psi(\theta)-\psi(\theta_0))]\}\,dH(\theta).$$

The mixture sequential probability ratio test, or mSPRT, first stops at $T^H(\alpha)=\inf\{n\ge1:\Lambda_n^H\ge1/\alpha\}$ and rejects exactly when this time is finite. An empty crossing set gives infinity. A user with maximum count $M\ge1$ and tolerance $0<\alpha<1$ instead observes $\min(T^H(\alpha),M)$ samples and rejects when $T^H(\alpha)\le M$. Thus a crossing at the last allowed sample still rejects. These are equations (7)–(9) and Section 5.1.

Formalization targets

The sole supporting milestone is equation (10), page 19. For every fixed admissible $H$ and every fixed alternative $\theta$, set

$$I(\theta,\theta_0)=(\theta-\theta_0)\psi'(\theta) -(\psi(\theta)-\psi(\theta_0)).$$

The claim is

$$\frac{T^H(\alpha)}{\log(1/\alpha)}\longrightarrow I(\theta,\theta_0)^{-1} \quad\text{in probability and in }L^2(P_\theta),\qquad\alpha\downarrow0.$$

For the goal, the power profile of a bounded rule is $\nu_R(\theta)=P_\theta(\delta_R=1)$ and its relative run length is $\rho_R(\theta)=E_\theta[T_R]/M$. A feasible competitor stops by $M$ almost surely, has Type I error at most $\alpha$, and has power at least the truncated mSPRT's power at every alternative. The competitor need not belong to a nested family of tests. Definition 3, page 21, defines

$$\phi(M,\alpha)=\inf_{R\ \mathrm{feasible}}\inf_{\theta\in\Theta\setminus\{\theta_0\}} \frac{\rho_R(\theta)}{\rho_H(\theta;\alpha,M)}.$$

The goal is the complete Theorem 2, page 21: if $\psi''$ is absolutely continuous on its parameter interval and finite on an open neighborhood of $\theta_0$, then, for every fixed admissible $H$,

$$\phi(M,\alpha)\longrightarrow1\quad\text{as }\alpha\to0,\quad M\to\infty, \quad M=O(\log(1/\alpha)).$$

The constant is exactly one. Both infima stay inside the limit. All qualifying paths are included, even when $M/\log(1/\alpha)$ tends to zero.

What the comparison would establish

The efficiency claim compares sample use with an entire class of decision rules, while requiring that competitors match power at every alternative. It therefore addresses a stronger question than the runtime of one test at one parameter. The mixture is fixed before the user's asymptotic choices; the first-order claim does not optimize a new mixture at each tolerance.

The source presents this as a theorem. The present formalization supplies open Lean statements, not completed proofs. It also records two gaps in the printed argument and a support ambiguity in its likelihood notation. Formal work can determine whether the complete printed target is provable or admits a counterexample. Those findings do not replace the goal with a repaired or restricted claim.

Why pointwise limits do not settle efficiency

Convergence of the runtime at each fixed alternative does not imply convergence after taking an infimum over all alternatives and all feasible rules. Alternatives can approach the null or move toward the boundary as the tolerance changes. The printed proof on pages 42–43 obtains a comparison at a selected alternative, which alone cannot lower-bound the full infimum. It also substitutes a parameter that need not approach zero into an expansion stated as the parameter tends to zero. These are identified proof gaps, not asserted counterexamples to the statistical theorem.

Formalization scope

The model reuses the published scalar exponential-family definition with scale one and zero base log density. An arbitrary reference measure is allowed; choosing $f_0(x)\,dx$ recovers every density family in the source. Observations may live on any measurable probability space, while the history sigma algebras are exactly those generated by the observed coordinates. Coordinate zero represents $X_1$.

Stopping times use extended natural numbers. Nonnegative expectations and both infima use extended nonnegative reals. Infinite stopping times are never replaced by zero. At valid finite horizons, positive sample counts give positive finite denominators; the mSPRT's error control supplies a feasible competitor. These facts must follow from the definitions rather than enter as assumptions. The milestone includes square integrability and almost-sure finiteness in its conclusion. The goal uses every valid sequence to express the joint limit.

Equation (7) is read as the exponential likelihood ratio after cancellation of the carrier density. This agrees with its quotient wherever defined. A carrier with disconnected support can give a sample mean where the printed quotient is $0/0$; that issue is recorded explicitly. No everywhere-positive carrier assumption is added. Definitions of binary decisions, positive-density mixtures, natural histories, and efficiency support further sequential-testing work.

Selected references

• R. Johari, L. Pekelis, and D. Walsh, Always Valid Inference: Continuous Monitoring of A/B Tests, arXiv preprint, 2019, arXiv:1512.04922v3, Sections 3 and 5.1–5.3, equation (10), Definition 3, Theorem 2, and Appendix A. All source numbers in this mission refer exclusively to this pinned version.

Motivation: removing time-discretization bias

A Monte Carlo price estimate averages discounted payoffs over simulated scenarios. Its statistical error can be assessed from the variation of those payoffs. When a continuous-time stochastic model is replaced by a finite time grid, a second error enters: the simulated distribution differs from the model distribution. Increasing the number of scenarios does not remove that bias at a fixed grid. Broadie and Kaya address this problem for stochastic volatility by constructing samples of terminal stock price and variance from their joint law. Their published paper develops the Heston construction first and then considers jump extensions and pricing applications. This mission concerns the complete Heston construction of §3 and its unbiased-pricing consequence.

Setting: stock price and square-root variance

The Heston model describes a stock price $S_q$ and its instantaneous variance $V_q$. Under the risk-neutral probability measure they solve

$$dS_q=rS_q\,dq+\sqrt{V_q}S_q\bigl(\rho\,dW_q^{(1)}+\sqrt{1-\rho^2}\,dW_q^{(2)}\bigr),$$ $$dV_q=\kappa(\theta-V_q)\,dq+\sigma_v\sqrt{V_q}\,dW_q^{(1)}.$$

Here $W^{(1)}$ and $W^{(2)}$ are independent standard Brownian motions. The real number $r$ is the risk-neutral drift, $\kappa>0$ is the speed of mean reversion, $\theta>0$ is the long-run variance, and $\sigma_v>0$ is the volatility of variance. The correlation $\rho$ ranges over the closed interval $[-1,1]$. These are the dynamics in (1)–(2), p. 218.

Fix arbitrary deterministic times $0\le u<t$, write $\Delta=t-u$, and start at $(s,v)$ with $s>0$ and $v\ge0$. The processes are continuous and adapted, with stochastic integrals interpreted locally in the Itô sense. The integrated variance is $A=\int_u^tV_q\,dq$. The dimension parameter $d=4\kappa\theta/\sigma_v^2$ is any positive real number. The regime in which variance can reach zero remains in scope; the condition $2\kappa\theta\ge\sigma_v^2$ is not imposed.

Formalization targets

The main target is equality of the joint laws of the original SDE and the paper's explicit ideal sampler:

$$\mathcal L(\widehat S,\widehat V)=\mathcal L(S_t,V_t).$$

For random starting states, this is an almost-everywhere equality of conditional probability measures given $(S_u,V_u)$. The sampler is defined independently: it draws a scaled real-degree noncentral chi-square variance, uses the explicit continued characteristic function and Fourier inverse CDF for integrated variance conditional on that sampled variance, recovers the first Brownian integral algebraically, and uses an independent standard Gaussian for the stock draw. This is the four-step algorithm and its completion in §3.3.

For any measurable payoff $f$ on the two terminal coordinates, put $g=e^{-r\Delta}f$ and $P_f=E[g(S_t,V_t)]$. Independent sampler repetitions give the ordinary empirical average $\widehat P_N$. Whenever $g$ is absolutely integrable, the target includes

$$E[\widehat P_N]=P_f\qquad(N\ge1).$$

For nonnegative payoffs, expectation equality is also stated with possibly infinite values. If $g$ has a finite second moment, write $\sigma_f^2=E[(g-P_f)^2]$. Then

$$\operatorname{MSE}(\widehat P_N)=\frac{\sigma_f^2}{N},\qquad \operatorname{RMSE}(\widehat P_N)=\frac{\sigma_f}{\sqrt N}.$$

Under the fixed per-path cost convention $s_{\rm budget}=cN$, $c>0$, the latter equals $\sigma_f\sqrt c/\sqrt{s_{\rm budget}}$. The asymptotic rate is $O(s_{\rm budget}^{-1/2})$, with the explicit coefficient fixed independently of sample count. This is the §1 cost convention and p. 219 standard-error identity. It is not a claim about the bit complexity of special-function evaluation.

Seven source displays supply the milestones: the stock exponential representation (6); the scaled noncentral chi-square transition law (8)–(9); the squared Bessel bridge transform (39); the square-root bridge Laplace transform (40); its characteristic-function counterpart (13); both Fourier inversion equalities (14); and Brownian-integral recovery (23). Each retains its coefficients and full parameter domain.

Significance: exact laws and statistical error

Equality of joint laws makes the pricing result applicable to payoffs depending on both terminal stock and terminal variance, a scope expressly described in §8. It also separates the assumptions needed for different conclusions: exact simulation is distributional, unbiased real-valued pricing needs an absolute first moment, and the RMS formula needs a second moment. These distinctions matter for unbounded payoffs.

The paper establishes these results mathematically. This mission supplies open Lean statements and concrete definitions for formalizing them; it does not claim that their proofs have already been checked. The reusable contributions include real-degree noncentral chi-square sampling, continuous endpoint bridge semantics, and a complex Bessel ratio that retains its branch and boundary conventions. The local Itô-integral foundation is reused from a published definition.

Difficulty: dependence, continuation, and boundary values

Knowing the marginal laws of terminal variance and integrated variance is insufficient. They are dependent, and the stock formula uses that dependence. Replacing the bridge draw by an independent marginal draw changes the joint law. Similarly, the conditional normal expression for the stock does not by itself prove that the inputs to that expression have the required distribution.

The characteristic expression (13) contains a modified Bessel function at a complex argument. The source explicitly requires continuation between branches in (22). Principal-branch evaluation alone can introduce a discontinuity. Zero variance endpoints create another difficulty: the raw numerator and denominator can both vanish or diverge, while their ratio has a meaningful continuous extension. Finally, Fourier inversion must establish a genuine continuous CDF and a valid inverse-transform draw; these properties cannot be supplied as premises.

Formalization scope

The original processes are defined by SDE integral equations on a usual filtered probability space. The published local Itô relation uses bounded predictable approximations and convergence in probability, without requiring global expected squared energy. The generic square-root processes are separate from the paper-specific multiplicative stock model. Neither definition contains a terminal distribution or sampler-correctness field.

Conditional laws at random states use regular conditional distributions almost everywhere. For deterministic endpoints, bridge laws are specified by weak limits of conditioning on shrinking positive-width terminal observation windows. Their existence is asserted in the bridge theorems. The Bessel quotient cancels the common endpoint power through the entire factor $H_\nu$ from (21); the continued logarithm tracks the frequency path. Both infinite Fourier integrals are represented by limits of truncated integrals, and quantile well-definedness is part of the inversion conclusion.

The sampler uses ideal real and complex operations. The finite trapezoidal sum and numerical tolerance discussion in §3.2 describe an approximation to that ideal construction. They are not an exact finite-precision implementation. Jump-model extensions, conditional variance reduction, Greeks, and forward-start pricing are separate results outside this mission's selected goal. Proof contributions can develop the stochastic, analytic, or probability-measure foundations without changing the selected statements or their domains.

Selected references

• Mark Broadie and Özgür Kaya, Exact Simulation of Stochastic Volatility and Other Affine Jump Diffusion Processes, Operations Research 54(2), 217–231, 2006. Published article. The mission uses this version throughout, especially §§2.1 and 3, the Appendix, and the statistical conventions in §§1–2.2.

Learning prices while selling limited inventory

A retailer must learn demand while selling a fixed stock over a finite season. A high price preserves inventory but may leave profitable sales unrealized. A low price can exhaust stock before later customers arrive. Learning is harder when some customers behave unlike the population whose demand the retailer wants to learn. Those customers can arrive in a concentrated block and can adapt to what has already happened. The problem studied by Chen and Wang asks for pricing rules whose revenue loss remains controlled without knowing the number of these outliers or whether inventory will bind at the unconstrained optimal price.

This mission concerns the paper's modular general-inventory result. Its inputs are two pricing policies with guarantees in the two opposite inventory regimes. Its target is the guarantee claimed for the particular randomized meta-policy that combines them. The input guarantees remain assumptions, rather than being replaced by guarantees for a specially chosen pair of implementations.

A continuous-price model with adaptive outliers

There are T selling periods and real initial inventory $x_0T$, where $0<x_0\le1$. Prices lie in a compact nonnegative interval $[\underline p,\overline p]$. The unknown typical demand curve $f_0$ decreases strictly from 1 to 0 across that interval. The curve and its inverse satisfy the two-sided Lipschitz assumptions printed in the paper. The demand-coordinate revenue, $r(d)=df_0^{-1}(d)$, is twice continuously differentiable on $(0,1)$, with $0<\sigma^2\le-r''(d)\le M^2$.

An adaptive adversary chooses whether each customer is an outlier and, if so, a measurable alternative demand curve into $[0,1]$. These choices can use the full past of prices, sales, demand curves and outlier indicators. They precede the current price decision. The seller sees only earlier prices and sales, together with its own private randomness. The total number of outliers is at most $\varepsilon T$ almost surely for every policy. A fixed positive α satisfies $\varepsilon\le T^{-\alpha}$. The seller does not receive ε, α, the typical curve, or the true inventory regime.

At a chosen price, sales are demand plus noise censored by the remaining physical stock. Sales belong to $[0,1]$, and revenue is price times actual sales. Noise has mean zero conditional on the current price, as stated in §3; independence across periods and mean zero conditional on the entire history are not assumed.

The clearance price is $p^c=f_0^{-1}(x_0)$, and the unconstrained revenue optimum $p^o$ maximizes $pf_0(p)$ over the continuous interval. The typical-demand fluid benchmark is

$$r^*=\max_{p\in[\underline p,\overline p]}p\min\{f_0(p),x_0\}.$$

Regret is $Tr^*$ minus expected cumulative actual revenue. The expectation includes both seller randomization and customer randomness. The model and inventory rate stay fixed as T grows.

Formalization targets

The supporting targets, in proof-use order, are the e-companion's Lemma EC.4, its Lemma EC.3, main-text Lemma 5, and Corollary EC.1. The first is the uniform martingale inequality

$$\Pr\{\exists n\ge1:S_n\ge a,\ V_n^2\le y\}\le\exp[-a^2/(2(y+ca))].$$

The next bounds the error in a sampled fixed-price demand average, using the corruption count within the selected periods and positive stock at their beginnings. Lemma 5 gives both simultaneous exploration-estimate errors, with every printed constant and its full $H_Z$ expression. Corollary EC.1 asserts

$$|\widehat p^c-p^c|+|\widehat p^o-p^o|\le0.2|p^o-p^c|$$

with probability $1-O(T^{-2})$ under its printed parameter and polynomial-threshold conditions.

The goal is Theorem 4, covering both strict regimes $p^c<p^o$ and $p^c>p^o$. If the two supplied policies have their respective uniform $\widetilde O(\varepsilon T+\sqrt{T''})$ regret guarantees, then the specified Algorithm 5 satisfies

$$R_{T,\varepsilon T}=\widetilde O(\varepsilon T+\sqrt T)$$

for sufficiently large T. The absolute subroutine corruption budget is εT. The excluded equality case stays excluded. The polynomial parameter dependence and logarithmic factors are represented with constants and degrees chosen before horizons, contamination levels and environments.

What the formalization contributes

The target transfers guarantees for policies that know their applicable inventory regime into a guarantee for the paper's specified combination. Its operational definitions separate reusable randomized observed-history policies from the pricing model, real inventory dynamics, exploration estimator and meta-policy. This makes the meaning of actual revenue and the seller's information available for inspection independently of any proof.

The source presents these results with proofs, but this mission supplies open Lean statements rather than completed machine-checked proofs. Source findings are retained separately: the printed exploration normalization admits a counterexample to Lemma 5, and the stated price-conditioned noise assumption admits a counterexample to Lemma EC.3. Those claims remain exactly the targets to prove or disprove; they are not silently replaced by corrected versions. Corollary EC.1 also retains a printed maximum whose use in the proof needs scrutiny.

Why the claim requires care

Exploration competes with revenue collection for the same physical inventory. A successful estimate obtained after stock has been depleted cannot restore the lost opportunity. Outliers can cluster early, and the two input policies need different conditions to make their guarantees applicable. Neither the regime estimates nor successful exploration can be assumed in a faithful statement. The distinction between conditioning noise on price and conditioning it on the whole past is also consequential: the latter would impose a stronger statistical model than the paper prints.

Formalization scope and conventions

All prices, sales and stock quantities are real. Time is indexed by elapsed periods starting at zero. The general policy interface takes only public initialization data, private randomness and observed price/sales history. Environment randomness ranges over arbitrary measurable spaces and is independent of the private tape; its response may depend on the current price. The almost-sure budget is required for every admissible policy. Measurability and integrability make expectations meaningful, without bounding uncensored noise.

Algorithm 4 uses the endpoint-inclusive grid and the printed estimate $N_3\widehat d(i)/T_0$, with $T_0=\lceil\sqrt T\rceil$. Ties use the lowest index. Pricing outside a selected exploration set uses a separate private tape, preserving fresh exploration draws. Algorithm 5 samples a private epoch schedule, uses its realized cardinality for the grid, and interleaves exploration with the selected input policy. The prior epoch's observations determine the next branch. Each subroutine receives the nominal epoch horizon and nominal stock allocation; its history advances only on its assigned periods. The nominal quota is checked between selling periods to determine subsequent prices; individual sales are censored by actual global stock, which is shared and never reset.

The source omits zero/singleton-grid behavior despite giving those events positive probability. The explicit completion returns the lower endpoint for both estimates and uses the lower price on a singleton grid. No event is excluded from the goal. Theorems 1–3 and the independent lower-bound Theorem 5 are outside this mission's dependency scope. The meta-policy's regret guarantee occurs only in the goal conclusion, never in its definition or an algorithm-validity assumption.

Selected references

• Xi Chen and Yining Wang, Robust Dynamic Pricing with Demand Learning in the Presence of Outlier Customers, Operations Research, DOI 10.1287/opre.2022.2280. The catalog uses the 2020 paper identifier; citations here use the supplied manuscript's pp. 10–13 and 29–32, not independently verified journal pagination.
• Xi Chen and Yining Wang, e-companion to Robust Dynamic Pricing with Demand Learning, accompanying the same DOI, publisher file opre.2022.2280.sm1.pdf, ec9–ec10 and ec13–ec17. Both pinned local PDFs belong to this single citation family.

Motivation

Retailers sometimes offer a discount on a game only after a customer buys a console. Such add-on discounts let the customer choose individual additional products while the retailer controls both the original prices and the conditional offers. A retailer with limited transaction history must learn purchase probabilities while choosing these prices. Offering discounts on only a limited number of products adds a selection decision to the pricing problem. Simchi-Levi, Sun and Zhang study this joint learning and optimization problem in arXiv:2005.00947v1. This mission concerns their UCB-Add-On regret theorem and the five supporting lemmas used in its argument.

Setting

A retailer has core products, numbered by a positive integer $N$, and supportive products, numbered by a positive integer $M$. Core prices belong to a finite nonempty menu $\Omega_c$. Original supportive prices belong to $\Omega_s$, and discounted supportive prices belong to $\Omega_a$. All prices are nonnegative real numbers. There is no rational-grid assumption. The nonnegative integer $S$ limits the number of discounted supportive products; it may be zero or exceed $M$.

A policy $\pi$ specifies a core price $p_n$ for each core product, an original price $s_m$ and discount price $a_m$ for each supportive product, and a Boolean selection $I_m$. Feasibility means $\sum_m I_m\le S$ and $a_m<s_m$ for every supportive product, including those not selected. The operational problem has at least one feasible policy.

The demand tables are arbitrary fixed functions with values in $[0,1]$. The mean primary purchases are $\alpha_n(p_n)$ for core products and $\alpha_{N+m}(s_m)$ for supportive products. Each core purchase creates an opportunity to buy each supportive product, with mean $\beta'_m(a_m)$ when selected and $\beta_m(s_m)$ otherwise. Fresh primary purchases are independent Bernoulli observations; conditional on those purchases, the add-on opportunities receive independent Bernoulli observations. A period can contain any number of core purchases from zero to $N$. There is no inventory depletion or assumption that a customer selects at most one core product.

The expected revenue is

$$R(\pi)=\sum_n\alpha_n(p_n)p_n+\sum_m\alpha_{N+m}(s_m)s_m+ \left(\sum_n\alpha_n(p_n)\right)\sum_m\left[I_m\beta'_m(a_m)a_m+(1-I_m)\beta_m(s_m)s_m\right].$$

The benchmark $R^*$ is the attained maximum over the feasible policies in equation (1). The same polynomial evaluates an algorithm output even if the printed procedure produces a tuple that fails the unconditional discount-price constraint.

Algorithm 1 optimizes supportive revenue at demand grid points, ranks the benefit of offering each discount, rounds core demand to the nearest multiple of $1/K$, and recovers maximizing policies from a backward dynamic program. Algorithm 2 estimates all four parameter families. Primary counters count periods; add-on counters count core-purchase opportunities. At episode start $t$, each positive-count upper confidence bound is $\min(1,\bar\alpha+\sqrt{2\log(t)/c})$, with the corresponding empirical mean for each family. Algorithm 1 receives these estimates and $K=\lceil\sqrt t/\varepsilon\rceil$. Its output is held until an associated counter doubles, including overshoots.

Formalization targets

Define $\widehat p=\max(\Omega_c\cup\Omega_s)$ and $U=\max(|\Omega_c|,|\Omega_s|,|\Omega_a|)$. Let $\lambda$ be the minimum probability of nonzero total primary demand over feasible policies, including primary supportive demand. Regret is the expectation of $\sum_{t=1}^T(R^*-R(\Pi_t))$ under the algorithm's own trajectory law.

The goal is Theorem 2, page 16, equation (7):

$$\operatorname{Regret}(T)=O\!\left(NM\widehat p\left[\lambda^{-1}\sqrt{UT\log T}+\varepsilon\sqrt T\right]\right).$$

One positive absolute multiplier precedes the instance and $\varepsilon$. The eventual horizon threshold may depend on the instance and $\varepsilon$, but precedes every controller and tie choice. At $\lambda=0$ the upper bound is infinite.

The milestones retain the source's use order: Lemma 4 bounds expected episode length by its starting time; Lemma 5 bounds total bad-event episode regret by a horizon-independent constant; Lemma 1 asserts the exact supportive Lipschitz constant $M\widehat p$; Lemma 3 asserts actual-revenue approximation error at most $\widehat p MN/K$; Lemma 6 bounds good-event episode regret by a constant times both terms of the displayed rate. The independent offline FPTAS theorem and lower-bound remark are outside this mission.

Significance

The regret claim quantifies the cumulative cost of learning demand while computing approximate pricing decisions. Its displayed dependence distinguishes the number of products, the number of candidate prices, the price scale and the approximation input. Keeping these factors explicit prevents an instance-dependent asymptotic constant from hiding the central claim of Theorem 2.

The formalization supplies concrete declarations for the pricing model, both algorithms, the observation law and the source's claims. The six theorem declarations are statements awaiting proofs or disproofs. Compiling them does not establish the printed results. In particular, the literal supportive subproblem has a counterexample to its claimed Lipschitz constant, and other source discrepancies require careful separation from the intended analysis.

Difficulty

Feedback for supportive add-on demand arrives only when a core purchase creates an opportunity. Those counts can remain zero even when total primary demand is always positive. Episode lengths and the histories at which confidence events are tested are random. Replacing this feedback by a policy-level reward observation changes the learning problem.

The source also leaves initialization and zero-start doubling unspecified. Its displayed bad event uses $2\log(t)/c$ without the square root in the algorithm. Equation (3) reverses the strict price inequality used in equation (1), while Algorithm 1's ordinary branch can select an original price with no smaller discount available. These issues are retained explicitly; a corrected algorithm or corrected lemma would be a separate result. In particular, completing an unseen profitable core price with UCB zero can leave it unexplored forever and give linear regret. The universal-completion targets include this case; the initialization insight records the explicit two-price example.

Formalization scope

Finite menus use injective real-valued labels and products use finite index types. Demand values zero and one are included. All rounding and maximizing ties are admitted. The generic probability-mass object is Mathlib's PMF; the paper-specific controller uses distributions on finite policy tuples and post-observation stopping probabilities. Recursively multiplied finite kernels define every finite-horizon expectation. No concentration, optimism, approximation error or regret inequality is included in a run condition.

Undefined zero-count UCB branches range over all causal values in $[0,1]$. Undefined zero-start stopping branches range over all causal almost surely finite positive completions, while every defined positive-count doubling stop is enforced. These are declared generalizations, not a favorable initialization convention. The bad event likewise includes every history-determined Boolean completion at zero counts. Its positive-count radius remains literal. Event contributions use indicator weighting at the actual episode-start history and truncate the final episode; full conditional episode length uses an extended nonnegative tail sum.

The printed supportive maximum has its own feasible set and nonemptiness condition. Operational benchmark feasibility is separate. This separation keeps the reversed-price counterexample expressible without imposing it on the online model. The concrete definitions support future proof and disproof work without assuming any of the target bounds.

Selected references

• David Simchi-Levi, Rui Sun and Huanan Zhang, Online Learning and Optimization for Revenue Management Problems with Add-on Discounts, arXiv preprint, 2020, arXiv:2005.00947v1, Sections 2–4, Algorithms 1–2, Lemmas 1, 3–6 and Theorem 2. PDF and printed pages agree for pages 1–33.

Learning while acting

A seller choosing prices may learn about demand from purchases while earning revenue from those same purchases. The hidden customer characteristic can range continuously, even when there are only a few prices and observations. A policy must therefore trade off present reward and information that affects later decisions. Describing every possible belief about a continuous parameter makes a direct dynamic program difficult to represent.

Hao Zhang's Dynamic Learning and Decision Making via Basis Weight Vectors studies a different representation: the reward of a continuation policy as a function of the hidden parameter. The exact result in Section 4.1 states that polynomial primitives permit the relevant family of these functions to be recovered through operations on finite coefficient vectors. This mission concerns that exact result, including its whole efficient frontier at every period.

Operational setting and the two frontiers

A parameter $\theta\in\Theta=[0,1]$ is selected before a horizon of $T$ decision periods and stays fixed. At each period an agent chooses an action from a finite nonempty set $A$ and receives a signal from a finite nonempty set $S$. Conditional on action $a$ and the parameter, signal $s$ has probability $p(s\mid\theta,a)$. These probabilities are nonnegative and sum to one. The associated reward $r(\theta,a,s)$ is real and may be unobserved. The discount factor satisfies $0<\delta\le1$.

A continuation policy is a finite tree whose root chooses an action and whose child is selected by the next signal. Its choices never observe $\theta$. Its continuation-value function $u(\theta)$ is its expected discounted reward conditional on that fixed parameter. A terminal continuation function supplies the boundary value. A finite efficient family of terminal functions is also permitted, covering the soft termination described in assumption (A2).

The positive-normal extreme frontier, written $\operatorname{PNEP}$, retains strictly exposed members of a finite set. For vectors in $\mathbb R^{d+1}$, an exposing normal $\rho$ has nonnegative coordinates summing to one. It must give its chosen member a strictly larger inner product than every distinct competitor. For functions on $[0,1]$, normals are all nonnegative square-integrable densities $\pi$ with integral one, and the comparison is $\int_0^1\pi(\theta)u(\theta)\,d\theta$. The two spaces have different families of normals.

The basis-weight representation uses monomials $\phi_i(\theta)=\theta^i$. A weight $w=(w_0,\ldots,w_d)$ represents $\Phi w=\sum_iw_i\phi_i$. Coefficients may be negative, even for a nonnegative probability function. Weight addition uses zero padding, and $a\otimes b$ is ordinary coefficient convolution. Assumption (A1) supplies weights for every probability and reward function. Assumption (A2) supplies weights for every terminal frontier member.

Exact formalization targets

The three supporting statements are Lemma 1, Corollary 1 and Lemma 3. The first retains both algebraic identities, including unequal vector lengths:

$$\Phi a+\Phi b=\Phi(a+b),\qquad (\Phi a)\odot(\Phi b)=\Phi(a\otimes b).$$

The second identifies expected-reward weights:

$$\bar r(a)=\Phi w_{\bar r}(a),\qquad w_{\bar r}(a)=\sum_{s\in S}w_p(a,s)\otimes w_r(a,s).$$

Here $\bar r(a)(\theta)=\sum_s p(s\mid\theta,a)r(\theta,a,s)$.

For a finite weight set $W$ and a nonnegative basis family, Lemma 3 says that every member of $\operatorname{PNEP}(\Phi W)$ is represented by a member of $\operatorname{PNEP}(W)$, and

$$\operatorname{PNEP}(\Phi W)=\operatorname{PNEP}(\Phi\operatorname{PNEP}(W)).$$

The goal is Theorem 1. Initialize $W_{T+1}^*=\{w(u):u\in U_{T+1}^*\}$. For every $t=1,\ldots,T$ and every $a\in A$, compute

$$W_t^*=\operatorname{PNEP}\left(\bigcup_{a\in A}W_t^*(a)\right),$$ $$W_t^*(a)=\operatorname{PNEP}\left(\left\{w_{\bar r}(a)+\delta\sum_{s\in S}w_p(a,s)\otimes w_{t+1}(s):w_{t+1}(s)\in W_{t+1}^*\ \forall s\right\}\right).$$

Then the independently defined function recursion of Eqs. (7)–(9) is recovered exactly:

$$U_t^*=\operatorname{PNEP}(\{\Phi w:w\in W_t^*\}).$$

Every period and action is retained. The terminal function family and terminal weight family are the prescribed boundary data. There is no approximation constant or degree truncation.

What the exact representation provides

The result replaces the manipulation of continuation functions with finite coefficient arithmetic while preserving the complete frontier relevant to density normals. It concerns an entire family of policies and priors, rather than a value for a single selected prior. The polynomial degree and number of candidate vectors can still grow; exact representability does not assert inexpensive computation. The source's approximation methods and empirical comparisons are separate from this claim (Zhang, Sections 4.3–5.6).

Formalization makes the two exposure notions, the information restriction on policies, and the terminal boundary explicit. The theorem declarations are proof targets; their compilation checks their types and definitions, not the validity of the asserted results. A completed development would provide checked algebraic and geometric statements for this representation.

Why the frontier comparison matters

Exact coefficient arithmetic alone does not establish the theorem. A coefficient vector can be exposed by a simplex normal while its evaluated function is dominated on the parameter interval. The paper illustrates this with the weights representing $1$, $\theta$ and $\theta^2$: every coordinate vector is exposed in coefficient space, but only the constant function survives function-space exposure. Consequently, the outer function-space PNEP in the recovery equality is essential (Zhang, p. 17, footnote 5).

The operational function recursion and the weight recursion are defined independently. Their agreement is a conclusion. Finite observations do not turn the hidden parameter into a finite state space, and probability nonnegativity does not imply coefficient nonnegativity.

Formalization scope and conventions

The interval is a subtype of the reals with its Lebesgue measure. Function equality is pointwise on that interval. The weight type is the real polynomial type, which represents finitely supported coefficients modulo trailing zeros. Finite normalized normals are tested at a common degree bound for each set; the bound is unrestricted. Polynomial multiplication supplies convolution. All primitive and generated functions are square integrable, so the density comparisons use integrable products.

Natural-number indices count remaining decisions: zero is terminal, and $n+1$ is computed from $n$. For a horizon $T$, the source period is $t=T-n$ at the update indexed by $n<T$. Lemma 3 permits arbitrary nonnegative L2 basis families, with independence interpreted in the source Hilbert space. The definition layer also includes policy trees, operational probabilities and rewards, terminal representations and both recursions.

Definition 4's component count is read as $\max(d_a,d_b)+1$, consistent with its zero-based indexing and its preceding example. This reading is recorded in insight I1 and in theorem differences. Gaussian, exponential, multivariate and spline extensions, numerical performance, and proofs of the approximation methods are outside this mission. Insights I2 and I3 retain the source findings about excluded appendices.

Selected references

• Hao Zhang, Dynamic Learning and Decision Making via Basis Weight Vectors, Operations Research, 2022. DOI 10.1287/opre.2021.2240. This mission uses the supplied published-basis artifact: model and definitions on PDF/printed pp. 7–16; Lemma 3 and Theorem 1 on p. 17; proofs on PDF pp. 52–53, EC pp. 8–9. The supplied PDF retains manuscript pagination and SSRN footers.

Choosing when to stop from simulated trajectories

An exercise decision can depend on today's observed state even when the evolution of that state depends on its history. Examples include deciding when to exercise an option whose reward depends on several asset prices or on earlier observations. A simulator can produce complete trajectories without providing the conditional distributions needed for a conventional dynamic programming calculation. Sturt studies an approach that uses those trajectories to select stopping policies. The present target concerns the exact structure of an optimizer of the resulting robust sample problem. It is a deterministic result about a fixed collection of paths, rather than a convergence assertion about the simulator. Sturt, §§2–3

Policies, rewards, and uncertainty boxes

A state is a vector in $X=\mathbb R^d$. A trajectory is a sequence $x=(x_1,\ldots,x_T)$ of states over a positive number $T$ of periods. A measurable exercise policy $\mu$ specifies a Borel stopping region $S_t\subseteq X$ at every period. The system stops when its current state first belongs to the corresponding region. Thus

$$\tau_\mu(y)=\min\{t\in\{1,\ldots,T\}:y_t\in S_t\},$$

where an empty minimum means $\infty$. The policy may change with time, but at each time its action uses only the current state. This definition does not assert that the stochastic process generating states is Markovian.

The reward $g(t,x)$ is a finite nonnegative number depending on the stopping period and the entire original trajectory. Dependence on both past and future coordinates is allowed. The reward for never stopping is $g(\infty,x)=0$. The structural result requires no global bound or continuity of $g$. These conventions are those of §2.1.

Fix a positive number $N$ of sample paths $x^1,\ldots,x^N$ and a radius $\epsilon\ge0$. The uncertainty box at period $t$ around sample $i$ is

$$U_t^i=\{z\in X:|z_a-x_{ta}^i|\le\epsilon\text{ for every coordinate }a\},\qquad U^i=\prod_{t=1}^T U_t^i.$$

Each box includes its boundary and contains its center, also when $\epsilon=0$. The full path uncertainty set is the Cartesian product, with no added dependence constraint between periods. The robust sample reward and its average are

$$r_i(\mu)=\inf_{y\in U^i}g(\tau_\mu(y),x^i),\qquad J(\mu)=\frac1N\sum_{i=1}^N r_i(\mu).$$

The adversary changes the input used by the stopping rule. The second argument of the reward remains the original sample $x^i$. This is problem (RO) in §2.2.

Exact attainment and the selected structural statements

Assign one period $\sigma^i\in\{1,\ldots,T\}$ to each sample. Define a policy by the assigned stopping regions

$$S_t^\sigma=\bigcup_{i:\sigma^i=t}U_t^i.$$

Let $M$ be the family of all policies produced by these assignments. It has at most $T^N$ members; assignments can yield identical policies. Every region is a finite union of closed boxes and hence is Borel measurable. The goal is the complete statement of Theorem 4, p.16:

$$\exists\mu_*\in M\quad\forall\mu\text{ measurable Markovian},\qquad J(\mu)\le J(\mu_*).$$

There is no approximation factor or error term. The comparison is against the entire class of admissible policies on $\mathbb R^d$.

Six source statements accompany this goal. Define terminal feasibility by $\forall i\,\exists t\,U_t^i\subseteq S_t$. Lemma 1 equates the unrestricted supremum with the supremum over these policies. For a terminal-feasible policy, write $\sigma^i(\mu)=\min\{t:U_t^i\subseteq S_t\}$. Lemma 2 gives the attained minimum

$$r_i(\mu)=\min\{g(t,x^i):t\le\sigma^i(\mu),\ U_t^i\cap S_t\ne\varnothing\}.$$

A pruned version has smaller stopping regions and preserves every earliest full-box stopping minimum. Lemma 3 asserts $r_i(\mu')\ge r_i(\mu)$ for each sample whenever $\mu'$ is a pruned version of $\mu$. For the assignment $\sigma^i=\sigma^i(\mu)$, Claim EC.6 asserts region inclusion, Claim EC.7 asserts equality of the full-box stopping minima, and Lemma 4 asserts the complete pruning relation. Both claims carry the terminal-feasibility and canonical-assignment preamble of Lemma 4. §3.2 and Appendix D, pp.16–17 and ec17–ec18

What the characterization supplies

The original decision variable is a collection of arbitrary measurable subsets of a continuum. The theorem ensures that an exact optimizer can nevertheless be represented by finitely many period assignments. This is the structural basis for the paper's subsequent combinatorial formulations and algorithms. The finite representation depends on the observed samples and radius; it does not impose a predetermined parametric family on all potential instances. §3, pp.13–18

Sturt supplies mathematical proofs of these statements. The present formalization supplies concrete definitions and compilable targets for formal proofs. The seven research results remain to be proved in Lean. The definition layer also supplies a reusable measurable policy interface separate from this particular robust objective, along with explicit first-exercise and never-exercise conventions.

Why a finite candidate family is not sufficient by itself

A finite nonempty family has a maximizer within that family, but this alone says nothing about policies outside it. The difficult comparison is with arbitrary Borel stopping regions. Shrinking such regions can change which periods an adversary can reach, so ordinary set inclusion does not by itself establish reward improvement. The full-box minima and the Cartesian structure of uncertainty are essential to the statements under consideration. Overlapping boxes, coincident samples, and contact at a box boundary all remain part of the problem. §3.2

Formalization scope and conventions

Lean represents periods and samples by Fin T and Fin N: index $k$ represents source index $k+1$. Positive $T$ and $N$ are part of the instance data. States are functions Fin d → ℝ, with their Borel measurable structure. The additional singleton state space at $d=0$ is admitted as a declared generalization. Finite rewards use nonnegative real numbers. An optional finite index represents a stopping time, with the absent index meaning infinity and yielding zero reward.

Infima, averages, and optimal values use nonnegative extended real numbers. Each sample reward is finite because its uncertainty set contains the sample and every reward is finite. More strongly, every possible sample payoff belongs to the finite set $\{0,g(1,x^i),\ldots,g(T,x^i)\}$; this supplies a common finite bound on all policy objectives. Thus the encoding introduces no infinite optimal value. Lemma 2 uses a least-element assertion, preserving the source's minimum attainment.

No optimization property is assumed in the model. The policy family is computed by the displayed union formula, and arbitrary comparison policies may continue forever. The model permits zero radius, zero rewards, duplicate paths, empty stopping regions, and rewards that distinguish trajectories with the same current state. The probability, density, and reward regularity assumptions of §2.4 concern separate convergence results and are absent here. Theorems beyond the selected dependency chain are outside this mission's scope. Formal proofs of the stated targets, using the common definitions and finite-set, measurable-set, and order infrastructure, are the remaining contributions.

Selected references

• Bradley Sturt, A Nonparametric Algorithm for Optimal Stopping Based on Robust Optimization, arXiv preprint, version 4, 20 March 2023. arXiv:2103.03300v4. Model: pp.6–7; family: p.14; Theorem 4 and Lemmas 1–4: pp.16–17; proofs and Claims EC.6–EC.7: pp.ec15–ec18 (PDF pp.55–58).

Comparing conservative decisions under uncertainty

A chance constrained program chooses a decision before observing uncertainty and limits the probability that its constraints fail. For example, a service system can allow a prescribed fraction of demand realizations to exceed its available capacity. The optimization problem combines a cost objective with a probability requirement. Even when each realized constraint is convex in the decision, the probability requirement need not define a convex feasible region. This motivates tractable conservative approximations. Jiang and Xie compare two such approximations, ALSO-X and conditional value-at-risk, in arXiv:2012.04763v4, §§2–3.

The question here concerns the best objective value admitted by each exact approximation. A smaller value means that the approximation imposes less conservatism in the minimization problem. The source's phrase “better than” explicitly means “at least as good as,” so the target permits equality. It does not claim strict improvement on every instance or a guarantee for every numerical implementation.

Decisions, laws and slack functions

Let the decision be $x\in\mathbb R^n$ and the uncertainty be $\xi\in\Xi\subseteq\mathbb R^m$, with an arbitrary probability law $P$. A positive finite family of real random constraint functions defines

$$g(x,\xi)=\max_i g_i(x,\xi).$$

Every random section is measurable. On a common set of probability one, each function of the decision is convex and lower semicontinuous. The decision set $X$ is nonempty, closed and convex, and is contained in a closed pointed convex cone $C$. The vector $c$ determines cost, while $0<\varepsilon<1$ is the permitted violation probability. The original problem minimizes $c^\top x$ subject to $x\in X$ and $P(g(x,\xi)\le0)\ge1-\varepsilon$. These are the objects of A1–A2 and (1), pp. 1–2.

A real budget $t$ restricts decisions to $D_t=\{x\in X:c^\top x\le t\}$. A functional slack is a measurable real function $s$ of the uncertainty; it is not a finite vector of sampled violations. The hinge-loss lower problem minimizes $E[s]$ over $x\in D_t$, $s\ge0$, and $s\ge g(x,\cdot)$ almost surely. Write $M^A_t$ for its complete set of optimal pairs.

The CVaR lower problem adds a real threshold $\beta\le0$. Its feasible triples satisfy $x\in D_t$ and $s\ge\beta$, $s\ge g(x,\cdot)$ almost surely, and its objective is

$$F(s,\beta)=E[s]-(1-\varepsilon)\beta.$$

Write $M^C_t$ for its complete set of minimizers. These lower problems are the ones displayed in equations (7) and (13), not merely pointwise risk functions evaluated at a fixed decision.

Formalization targets

Define the successful budget sets by

$$\begin{aligned} T_A&=\{t:\exists(x,s)\in M^A_t,\ P(s=0)\ge1-\varepsilon\},\\ T_C&=\{t:\exists(x,s,\beta)\in M^C_t,\ F(s,\beta)\le0\}. \end{aligned}$$

The goal is Theorem 1, p. 13: under A1–A2,

$$v^A:=\inf T_A\ \le\ v^{CVaR}:=\inf T_C.$$

The comparison constant is exactly one and there is no additive tolerance.

The two milestones are the printed necessary-and-sufficient optimality characterizations in Appendix A.4, p. 42, in their source order. With $f_\alpha(y)=E[\alpha g(y,\cdot)]$, (KKT1) asserts that CVaR optimality is equivalent to the existence of multipliers satisfying

$$\begin{gathered} -\pi c\in\partial f_\alpha(x)+N_X(x),\quad E[\mu]\le1-\varepsilon,\quad\mu+\alpha=1,\\ \alpha\perp(s-g),\quad\pi\perp(t-c^\top x),\quad\mu\perp(s-\beta),\quad\beta\le0,\quad x\in X. \end{gathered}$$

The corresponding hinge characterization (KKT2) asserts

$$\begin{gathered} -\pi c\in\partial f_\alpha(x)+N_X(x),\quad\mu+\alpha=1,\quad x\in X,\\ \alpha\perp(s-g),\quad\pi\perp(t-c^\top x),\quad\mu\perp s. \end{gathered}$$

Complementarity includes nonnegativity of both quantities and their zero product. Random equations hold almost surely. Both characterizations include multiplier existence and both directions of the equivalence.

What the comparison establishes

The claimed ordering says that the exact ALSO-X formulation admits an objective value at least as favorable as the CVaR formulation under the stated convexity assumptions. It compares complete optimization models, including lower-level optimality and upper-level acceptance. It does not compare just the expected positive losses at one decision, nor does it quantify an approximation error relative to the original chance constrained optimum. The source treats algorithmic tolerance separately in Corollary 2, which is outside this mission.

Formalizing these claims also makes their domains and the distinction between feasibility and attainment explicit. The statement modules compile, but the three source claims have not been proved in Lean. Two source findings accompany the mission: (KKT1) lacks beta complementarity and is not sufficient, and the unqualified multiplier-existence assertion underlying (KKT2) fails at a boundary budget. These findings concern the printed claims and proof; they do not constitute a disproof of Theorem 1. The target statements retain the source claims so that their mathematical status remains visible.

The difficulty of exact lower-level optimality

The inclusion of the hinge lower problem among the CVaR choices at $\beta=0$ does not itself establish the desired outer-value ordering. The two upper levels use different acceptance conditions, and both require actual optimal lower-level decisions. A comparison of lower objective infima cannot replace those requirements. Infinite expectations and nonattained optima also require care under arbitrary laws and unbounded decision sets.

The source's KKT route introduces a further issue: A1–A2 do not provide the multiplier existence asserted on p. 42. The difficulty is therefore partly an audit of the source's stated reasoning, in addition to the construction of stochastic convex-analysis infrastructure. Adding a Slater assumption would change the requested theorem.

Formalization scope

The development uses finite real coordinate spaces and Mathlib's convex cones and measure theory. Generic definitions of extended expectations, normal cones, subdifferentials and complementarity are separate from the paper's data and optimization models. The law of the measurable random vector encodes the original probability space without restricting its distribution to discrete samples. All positive finite counts of constraints are represented.

Outer values lie in the extended reals: the empty budget set has infimum $+\infty$, and an unbounded-below set has infimum $-\infty$. The nonnegative slack expectation is an extended integral. On the CVaR feasible set the objective is computed as $\varepsilon\beta+E[(s-\beta)_+]$, avoiding an undefined signed integral. Weighted signed expectations used in stationarity explicitly mark an infinite-positive-minus-infinite-negative expression as undefined; subgradients require a finite value at the candidate and inequalities on the defined domain.

A lower optimum means feasibility and comparison with every feasible competitor. Ties remain available for the existential upper-level choice. No global integrability, uniqueness, Slater condition, or certificate assumption is attached to the goal. The local A1–A2 wording controls over the global preamble's additional A3. Proofs, disproofs of the source milestones, and separately identified corrected variants can build on these definitions; a corrected variant does not replace a source target.

Selected references

• Nan Jiang and Weijun Xie, ALSO-X and ALSO-X+: Better Convex Approximations for Chance Constrained Programs, preprint, arXiv:2012.04763v4, 14 October 2021. Pinned source. Models and assumptions: pp. 1–2, 5–7, 12–13; Theorem 1: p. 13; Appendix A.4: pp. 41–43. All numbering refers to this version.

Motivation

A free-to-play multiplayer game earns subscription revenue only if players value the premium experience enough to pay for it. Yet converting free players into premium players also changes the experience of everyone else. Premium players may enjoy owning items that others lack, while free players may dislike comparisons with premium players. Advertising attracts new players, but its expense must be recovered during the game's finite lifespan. These interactions create a problem in which present revenue and future population growth respond to the same subscription price.

Mai and Hu (2022) study this interaction through a continuous-time model of social comparison, population growth, and operating profit. This mission concerns their main optimal-policy claim, Proposition 3, and its two numbered equilibrium dependencies, Lemmas 1 and 2. The target includes the full advertising and pricing trajectories in both unequal social-comparison regimes.

Setting

The market has total mass one. The active population $n(t)$ is a fraction in $[0,1]$, initially zero. Players receive a base utility $v$. A premium player observing a free player receives a downward-comparison benefit $\alpha_d$, whereas a free player observing a premium player suffers an upward-comparison loss $\alpha_u$. Both parameters are positive and less than $v$. Direct premium utility is normalized to zero, and the equality case $\alpha_d=\alpha_u$ is excluded, following the source.

If the premium share is $s$, the subscription price rate is $p$, and population is positive, free and premium utilities are

$$\Pi_F=v-s\alpha_u-1/n,\qquad \Pi_P=v+(1-s)\alpha_d-p-1/n.$$

A stable premium share satisfies one of three conditions: everyone is free and strictly prefers that status; everyone is premium and strictly prefers that status; or an interior share equalizes utilities and a marginal increase in premium participation hurts premium players more than free players. When several stable shares exist, players select the equilibrium with the highest utility. The common friction term cancels in these comparisons.

The printed response $S(p)$ is defined separately from the claim of stability. For $\alpha_d>\alpha_u$, it is one below $\alpha_u$, equals $(\alpha_d-p)/(\alpha_d-\alpha_u)$ on the inclusive interval $[\alpha_u,\alpha_d]$, and is zero above $\alpha_d$. For $\alpha_d<\alpha_u$, it is one at prices at most $\alpha_d$ and zero above that threshold.

Advertising strength $a(t)$ and price $p(t)$ are nonnegative measurable controls. Average utility excluding friction is

$$B(p)=v+S(p)(1-S(p))(\alpha_d-\alpha_u)-S(p)p.$$

The population follows the nonsingular form of the source's dynamics,

$$n'(t)=[a(t)+B(p(t))n(t)-1][1-n(t)].$$

This equation also specifies behavior at zero population. In particular, its drift there is $a-1$. Advertising has a twice differentiable cost $C$ with positive first and second derivatives on its nonnegative domain. For finite horizon $T>0$ and discount rate $r\ge0$, operating profit is

$$J(a,p,n)=\int_0^T[n(t)S(p(t))p(t)-C(a(t))]e^{-rt}\,dt.$$

Global optimality compares this quantity with every admissible control and trajectory, as in Problem (3), pp. 13–14.

Formalization targets

Lemma 1 claims that, when $\alpha_d>\alpha_u$, the stable shares are exactly the printed response. The middle share lies in $[0,1]$ and strictly decreases with price on $[\alpha_u,\alpha_d]$. Lemma 2 claims that, when $\alpha_d<\alpha_u$, the player-preferred stable shares are exactly the printed response. Both targets assert existence, through their two-way characterizations, including all stated boundary prices.

The goal, Proposition 3, asserts an attained globally optimal policy with strictly declining advertising and

$$a^*(T)=\lim_{t\uparrow T}a^*(t)=0.$$

It has an introduction threshold $\tau\in[0,T)$, possibly zero. Per-player payment $S(p^*(t))p^*(t)$ is zero before the threshold and positive after it. If $\alpha_d>\alpha_u$, price strictly decreases after introduction, with

$$p^*(\tau)=\lim_{t\downarrow\tau}p^*(t)=\alpha_d,\qquad p^*(T)=\lim_{t\uparrow T}p^*(t)=\max(\alpha_d/2,\alpha_u).$$

If $\alpha_d<\alpha_u$, price is identically $\alpha_d$ on $[\tau,T]$. No uniqueness is asserted. These are the exact endpoint prices and both regimes of Proposition 3, p. 14, with strict price decrease explicitly stated in the discussion on p. 15.

Significance

The source's claim describes when a developer starts charging and how its advertising and subscription price evolve. The downward-dominant regime allows scarcity of premium participation to influence population growth. The upward-dominant regime instead selects either universal premium participation or none, leading to a different asserted price path.

The formalization separates behavioral equilibrium, the stipulated population response, and global optimization. This distinction matters because a wrong equilibrium claim must not become an inconsistent assumption from which an optimal-control result follows automatically. The definitions are concrete, and the three theorem statements are open proof or disproof targets. There are no machine-checked proofs of those targets in this mission.

The source claims are preserved even where the source has defects. Lemma 1's inclusive boundary prices conflict with its strict definition of stability. The optimal-control proof has a discount-rate gap and a terminal division by zero; it also contains a payoff typo and a conflict between strict price decrease and a clipped formula. These findings are documented individually in the accompanying insights, without replacing the source targets by repaired claims.

Difficulty

The central issue is global optimization over time-dependent controls, rather than maximization of instantaneous revenue. Changes in price alter both revenue and population growth. The admissible set also contains the physical state boundary and unbounded advertising controls. Necessary optimality conditions alone do not state the required comparison against every policy.

Boundary conventions matter independently of analytic difficulty. The response must retain the source's inclusive middle price interval while stability retains its strict endpoint tests. The initial population is zero although the original utility expression contains reciprocal population. Endpoint prices must describe the path's limiting behavior, rather than arbitrary values assigned at individual times.

Formalization scope

Four definition items provide a general scalar control system, the player model, the advertising-cost class, and Problem (3). The paper-specific system instantiates the general trajectory definition. An integrable-drift integral equation represents absolutely continuous state paths. Controls are measurable for completed Lebesgue measure; their values outside the horizon are irrelevant. Almost-everywhere equivalent controls describe the same optimization choice, while the asserted path shape belongs to a chosen representative.

Profit uses an extended nonnegative integral of discounted $C(a)-C(0)$ together with the finite baseline cost. Thus infinite expenditure has profit $-\infty$ and cannot acquire a profitable default value. Revenue integrability is explicit. No normalization of $C(0)$, quadratic specialization, coercivity condition, control bound, small-discount condition, or positive initial population is imposed.

The advertising word “decreases” receives the stronger strict reading specified for this mission. One-sided endpoint limits prevent isolated assignments from manufacturing the claimed paths. These conventions are declared in each affected theorem's differences list. The mission's scope excludes the paper's independent matchmaking, partial-subscription, liquidity, and player-budget extensions.

Selected references

• Yunke Mai and Bin Hu, Optimizing Free-to-Play Multiplayer Games with Premium Subscription, Management Science, 2022. DOI: 10.1287/mnsc.2022.4510. Published-basis source with internal printed pages 1–39; Lemmas 1–2 on p. 8, Proposition 3 on p. 14, and its proof on pp. 34–37. Printed and PDF page indices coincide.

Learning while allocating scarce inventory

An online platform must allocate resources before it knows which customers will arrive later. Advertising budgets, limited product inventories and workers' task opportunities can all be exhausted by early decisions. When the probabilities of a successful allocation are also unknown, a platform must learn from the same interactions that consume its scarce resources. Reserving inventory for future customers and gathering useful observations are therefore coupled decisions.

Cheung, Ma, Simchi-Levi and Wang introduce Inventory Balancing with Online Learning (IBOL) to separate the inventory mechanism from the choice of learning algorithm. Their general guarantee relates the physical revenue of the allocation process to a linear-programming benchmark and a particular learning-regret quantity. This mission formalizes that framework result, Theorem 1, with its exact finite-capacity coefficient, rather than an application-specific oracle analysis. The source is the pinned preprint arXiv:1810.05640v2, Sections 2–4 and Appendix A.2.

Model, algorithm and benchmark

There are $n>0$ resources. Resource $i$ has positive integer capacity $b_i$ and earns reward $r_i\in(0,1]$ each time one unit is consumed. Inventory is not replenished. Customers arrive over a finite horizon $T>0$. Each arrival reveals a context $x_t$ from a known finite set. The context sequence is arbitrary but fixed by an oblivious adversary before the run. The algorithm receives the current context and past observations, without future arrivals or the horizon as inputs.

The action space $A$ is general. Given context $x$ and action $a$, a fixed unknown distribution $\rho_{x,a}$ produces a Boolean vector $y\in\{0,1\}^n$. Several coordinates may be one, and coordinates may be correlated. Write $p_{x,a,i}=\mathbb E_{\rho_{x,a}}[y_i]$. The chosen action generates a fresh conditional sample; outcomes for unchosen actions are unobserved. A successful coordinate consumes one unit only if inventory remains. Feedback is still observed for depleted resources. These are the model conventions in Section 2, pages 8–10.

Let $N_i^{t-1}$ count consumed units before round $t$. IBOL uses the perturbed potential

$$\Psi_\epsilon(u)=\frac{e^{(1+\epsilon)u}-1}{e^{1+\epsilon}-1}$$

to assign discounted rewards $r_i^t=r_i(1-\Psi_\epsilon(N_i^{t-1}/b_i))$. An arbitrary randomized bandit oracle receives the ordered history of observed triples, $x_t$ and $(r_i^t)_i$, and returns $a_t$. No maximization property or particular regret bound is required of the oracle. These operations specify Algorithm 1 in Section 3, pages 12–16.

Physical revenue is

$$\mathrm{ALG}=\sum_{t=1}^T\sum_i r_i y_{t,i}\mathbf1\{N_i^{t-1}<b_i\}.$$

The auxiliary mean reward is $R^t(a)=\sum_i r_i^t p_{x_t,a,i}$. Its dynamic comparator evaluates the best action at the very same realized inventory. The relaxed regret is the signed quantity

$$\mathrm{Reg}_\epsilon=\mathbb E\sum_{t=1}^T\left[\sup_{a\in A}R^t(a)-(1+\epsilon)R^t(a_t)\right].$$

It can be negative. It is neither regret against a fixed action nor the revenue gap to an independently run optimal allocation policy.

The LP benchmark chooses a probability allocation $s_t$ over actions in each period. It maximizes $\sum_{t,i}\int_A r_i p_{x_t,a,i}\,ds_t(a)$ subject to $\sum_t\int_A p_{x_t,a,i}\,ds_t(a)\le b_i$ for every resource. Each measure has total mass exactly one. Its optimal value is $\mathrm{OPT}$. For discrete actions these integrals recover equations (9)–(12) of the source.

Formalization targets

The goal is Theorem 1 on page 17, equations (13)–(14). For every model, oblivious arrival sequence, randomized oracle and $\epsilon\in[0,1]$,

$$\mathbb E[\mathrm{ALG}]\ge f_\Psi(\{b_i\},\epsilon)\bigl(\mathrm{OPT}-\mathrm{Reg}_\epsilon\bigr),$$

where the exact coefficient is

$$f_\Psi(\{b_i\},\epsilon)=\min_i\frac{1-e^{-(1+\epsilon)}}{(b_i+1+\epsilon)(1-e^{-(1+\epsilon)/b_i})}.$$

The formal extended-order statement is $\mathrm{OPT}\le\mathbb E[\mathrm{ALG}]/f_\Psi+\mathrm{Reg}_\epsilon$. Since $f_\Psi>0$, this is equivalent to the displayed guarantee whenever the LP value is finite.

There are two supporting milestones, both with the full inherited domain $\epsilon\ge0$. Claim 1, page 40, asserts that $\Lambda_i=r_i\Psi_\epsilon(N_i^T/b_i)$ and $\Gamma_t=\sup_a R^t(a)$ form a feasible solution to the printed dual for every realized path, and that

$$\mathrm{OPT}\le\mathbb E\left[\sum_t\Gamma_t+\sum_i b_i\Lambda_i\right].$$

Lemma 4, page 41, asserts for every positive integer $b$ and $N\in\{0,\ldots,b\}$ that

$$\frac{\Psi_\epsilon(\min\{b,N+1\}/b)-\Psi_\epsilon(N/b)}{1/b} +(1+\epsilon)(1-\Psi_\epsilon(N/b)) \le\mathbf1\{N<b\}\frac{(b+1+\epsilon)(1-e^{-(1+\epsilon)/b})}{1-e^{-(1+\epsilon)}}.$$

The two milestones are the numbered dependencies in Appendix A.2. Application-specific UCB and LazyUCB guarantees are outside this mission.

What the guarantee provides

The theorem gives an interface between a learning algorithm and an allocation guarantee: the oracle's relaxed regret enters a precise physical-revenue bound. Its coefficient retains every resource capacity and the exploitation parameter. At unit capacity and $\epsilon=0$, the resource coefficient is $1/2$; no large-inventory approximation is needed to interpret the target.

The paper supplies a mathematical proof. This mission supplies compiled statements and concrete definitions for a Lean proof of that result; the three theorem declarations remain open. The reusable outputs include a probability-measure packing LP and a model of randomized policies with correlated vector feedback. Establishing the stated theorems in Lean remains the solver's task.

Why the formal proof needs care

Discounted rewards change with realized inventory, which depends on earlier actions and outcomes. Treating the auxiliary reward sequence as independent would therefore lose the process that the theorem concerns. Likewise, assuming that the oracle selects an actual maximizer would remove the learning contribution from the statement.

Several boundary cases affect the mathematics. Resources at capacity still produce feedback, although their physical and discounted rewards vanish. Relaxed regret need not be nonnegative. The discrete inventory grid includes its depleted endpoint. A general action space need not admit a best action, and the equality-constrained primal LP need not be feasible when there is no zero-consumption action. The definitions retain these cases without inserting extra optimization or feasibility assumptions.

Formalization scope

Resources and finite contexts use finite index types; capacities are positive naturals. Histories carry the usual measurable structure obtained from the finite product space at each possible length. The run is built by successive probability-kernel sampling of an action and then its outcome. The oracle receives only observed history, current context and discounted rewards.

Action integrals extend the printed sums to general measurable spaces. Every discrete source allocation is included. Best-action suprema agree with the printed maxima whenever attained and additionally cover unattained values. The LP value uses extended reals, with $-\infty$ for an empty feasible set. No indeterminate extended-real subtraction appears in the theorem. Claim 1 also asserts pathwise feasibility for arbitrary length-$T$ observation strings, including probability-zero strings generated by the same physical update rule.

All objectives, coefficients, policies and certificates are constructed from data. Neither a performance bound nor dual feasibility is packaged as a model assumption. Mathlib supplies kernels, measures, integrals, finite sums, exponentials and order operations. The separate definition modules distinguish the general LP from its inventory-specific instance. The explicit history definition on page 15 determines the indexing used in Algorithm 1; the shifted update indices in its printed line 9 are recorded as a source finding.

Selected references

• Wang Chi Cheung, Will Ma, David Simchi-Levi and Xinshang Wang, Inventory Balancing with Online Learning, arXiv preprint, version 2, 30 August 2021. arXiv:1810.05640v2. All theorem indices and page references in this mission use this artifact.