Motivation

A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.

Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret $O\big((\log\log n)(\log n)^{1/2}/n^{1/2}\big)$. The paper's lower bound for parametric families (Proposition 4) is of order $n^{-1/2}$, so the rate is optimal up to logarithmic factors.

Setting

Market. Prices lie in $[\underline p,\overline p]\cup\{p_\infty\}$ with $0<\underline p<\overline p<p_\infty$. Posting the off price $p_\infty$ stops demand. The seller starts with inventory $x>0$ and sells over the horizon $[0,T]$, $T>0$.

Demand. A demand function $\lambda$ maps a price to a demand rate. The class $\mathcal L(M,\underline K,\overline K,m)$ consists of the functions that are non-increasing with an inverse $\gamma$ on $[\underline p,\overline p]$, have a concave revenue rate $r(l)=l\gamma(l)$, are bounded by $M$, are $\overline K$-Lipschitz with a $\underline K^{-1}$-Lipschitz inverse, and attain a revenue rate $\max_p p\lambda(p)\ge m$. The parametric family is $\lambda(p;\theta)$, $\theta\in\Theta=[\theta_{\mathrm{lo}},\theta_{\mathrm{hi}}]$, with every member in the class (Assumption 1). Assumption 2 adds a test price $p_1$, differentiability of $\sqrt{\lambda(p_1;\cdot)}$ and the Lipschitz bound $|\lambda(p;\theta)-\lambda(p;\theta')|\le\overline K_2|\theta-\theta'|$. Assumption 3 requires $\inf_{p,\theta}\lambda(p;\theta)>l_0>0$ and an $\alpha$-Lipschitz solution map $d\mapsto g(p,d)$ of the equation $\lambda(p;\cdot)=d$.

Demand process. Let $N$ be a unit-rate Poisson process. Under a price path $p(\cdot)$ and parameter $\theta^*$, the cumulative demand up to time $t$ is $N\big(\int_0^t\lambda(p(s);\theta^*)\,ds\big)$. Sales stop when the inventory runs out.

Benchmark and regret. The deterministic relaxation $J^D(x,T\mid\theta)$ is the supremum of $\int_0^T p(s)\lambda(p(s);\theta)\,ds$ over price paths with $\int_0^T\lambda(p(s);\theta)\,ds\le x$. In the market of size $n$ the inventory is $nx$ and the demand $n\lambda$. If $J^\pi_n(x,T;\theta)$ is the expected revenue of a policy $\pi$, its regret is $\mathcal R^\pi_n=1-J^\pi_n/J^D_n$.

Algorithm 3. Start from $\hat p_1=p_1$ and use stages of lengths $\Delta^{(1)}_n,\dots,\Delta^{(\ell_n)}_n$ summing to $T$. Stage $i$ applies $\hat p_i$, estimates the demand rate $\hat d_i$ from the stage's demand, solves for $\hat\theta_i=g(\hat p_i,\hat d_i)$, and sets $\hat p_{i+1}=\max\{p^u(\hat\theta_i),p^c(\hat\theta_i)\}$. Here $p^u(\theta)$ maximizes $p\lambda(p;\theta)$ and $p^c(\theta)$ minimizes $|\lambda(p;\theta)-x/T|$. The tuning (19)–(20) is $\ell_n=(\log2)^{-1}\log\log n$ stages with $\Delta^{(m)}_n=\beta_n n^{(a_{\ell_n}/a_m)-1}$ and $a_m=2^{m-1}/(2^m-1)$.

Formalization targets

Goal: Proposition 5

$$\exists\,C>0,\ \exists\,n_0,\quad \forall n\ge n_0,\ \forall\theta\in\Theta:\qquad \mathcal R^{\pi_n}_n(x,T;\theta)\le C\,\frac{(\log\log n)(\log n)^{1/2}}{n^{1/2}} .$$

The constants are uniform in $\theta$ and $n$. This is the paper's (21): $\sup_\theta\mathcal R^{\pi}_n=O(\cdot)$.

Milestones, in proof order

1. Fact 1: $J^D_n=nJ^D$ and $J^D\ge m\min\{T,x/M\}$ on the class.
2. Lemma 1: the deterministic relaxation is solved by the fixed price $p^D=\max\{p^u,p^c\}$.
3. Lemma 2: Poisson deviation bounds at scale $(\log n/r_n)^{1/2}$.
4. (A-27): a revenue lower bound that splits the loss into stage-wise terms and an overflow term.
5. The per-stage revenue gap $r(p^D)-\mathbb E\,r(\hat p_i)\le C_2(n\Delta^{(i-1)}_n)^{-1/2}$.
6. (A-30): the stage-$i$ demand rate rarely exceeds the run-out rate.
7. The overflow bound $\mathbb E[(Y_n-nx)^+]\le nC_8(\log n)^{1/2}n^{a_{\ell_n}-1}$.
8. (A-31): the revenue ratio before the exponents are evaluated.
9. The rate estimate $n^{a_{\ell_n}-1}\le e\,n^{-1/2}$.

Milestones 6–8 hold in the case $\lambda(\overline p;\theta^*)\le x/T$, the only case the paper's proof treats in detail.

Significance

Proposition 5 shows that with one unknown parameter, learning while earning reaches the $n^{-1/2}$ rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only $n^{-1/4}$ and $n^{-1/3}$. The paper leaves open whether the multi-parameter case attains the lower bound.

The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.

The result is proved in the paper, but parts of the proof are only sketched. The case $\lambda(\overline p;\theta^*)>x/T$ is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.

Difficulty

The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries $\Lambda_i=\sum_{j\le i}n\lambda(\hat p_j;\theta^*)\Delta^{(j)}_n$ depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses $\Delta^{(i)}_n/(n\Delta^{(i-1)}_n)^{1/2}$ are all of the same order. That balance has to be checked exactly, including the rounding of $\ell_n$ to an integer.

Formalization scope

• Poisson process. A structure on an arbitrary probability space: $N(0)=0$, monotone right-continuous paths, measurable marginals, Poisson increments, and independent increments over finite partitions. No process is published on the platform.
• Class and family. Conditions on $\lambda$ are imposed on $[\underline p,\overline p]\cup\{p_\infty\}$, the only prices a path uses. The inverse $\gamma$ is Function.invFunOn. $\Theta$ is a nonempty closed interval of $\mathbb R$.
• Assumption 3. As printed it cannot hold for $d>\sup_\theta\lambda(p;\theta)$. It is read as an $\alpha$-Lipschitz map $g(p,\cdot):[0,\infty)\to\Theta$ that inverts $\lambda(p;\cdot)$ on $\Theta$. $g$ is jointly measurable, so that estimates at random prices are random variables.
• Selections. $p^u,p^c$ are any measurable selections of the maximizer and minimizer; the statements hold for each.
• Inventory. The inventory is $\lfloor nx\rfloor$ units, and sales are capped cumulative counts.
• Time change. Eq. (1) is applied stage by stage with random stage boundaries.
• Typos. In Algorithm 3, "$\lambda(p_i,\theta)$" is read as $\lambda(\hat p_i;\theta)$ and "$x/t$" as $x/T$.
• Stages. $\ell_n=\lceil\log_2\log n\rceil$.
• Integrals. Expectations are lower Lebesgue integrals of nonnegative quantities, converted to reals. The relaxation is a real supremum over measurable paths.
• Asymptotics. The $O(\cdot)$ is rendered with an explicit $n_0$. The clause "asymptotically optimal" is omitted, since it needs the second half of Lemma 1.
• Ruled out. Each of the following would trivialize the statement: removing the inventory cap, replacing the random stage boundaries by deterministic ones, fixing $\theta$, letting $C$ depend on $\theta$, or using a non-measurable selection (whose expectation would be a junk value).

Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.

Selected references

• O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

Why learn demand while pricing?

A seller with a fixed inventory must choose prices before knowing how customers respond to them. A price that earns a high margin can sell too slowly; a price that sells quickly can exhaust stock before the selling season ends. Learning demand uses time and inventory, so the seller must account for the cost of its own experiments. This mission formalizes the parametric policy and regret bound of Besbes and Zeevi (2009), Proposition 3. Their setting differs from a finite-arm bandit: the permitted ordinary prices form an interval, customer arrivals are random, and the available stock caps total sales.

The paper first analyzes a nonparametric class with a slower upper bound in Proposition 1, then imposes a known finite-dimensional form on the unknown demand curve in Section 5. Proposition 3 shows how that additional information improves the regret rate for its Algorithm 2. The authors also prove a lower bound for a suitable parametric family in Proposition 4; that result is outside this mission's capstone, which concerns the performance guarantee of the concrete policy.

Market, demand, and policy

The selling horizon has length $T>0$, and the initial stock is $x>0$. An ordinary price $p$ lies in $[\underline p,\overline p]$, with $0<\underline p<\overline p$. The special price $p_\infty>0$ stops demand. At parameter $\theta\in\Theta\subseteq\mathbb R^k$, the demand rate is $\lambda(p;\theta)\ge0$. The parameter set $\Theta$ is nonempty, compact, and convex; $k$ is positive. The seller knows the family $\lambda(\cdot;\theta)$ but does not know the true parameter $\theta^*$.

For each parameter, demand is nonincreasing in the price and has an inverse $\gamma(\cdot;\theta)$ on the attainable rate interval. The rate revenue is $r(\ell;\theta)=\ell\gamma(\ell;\theta)$, a concave function of the rate. Every member of the family satisfies Assumption 1 with the same positive constants $M,\underline K,\overline K,m$: demand is at most $M$, its price variation is at most $\overline K$ times the price difference, its inverse is $\underline K^{-1}$-Lipschitz, and some ordinary price earns revenue rate at least $m$. These conditions define the class in which the bound is uniform. See §§3–4.2 of the source.

Customer requests follow a unit-rate Poisson process $N$ run on a demand-dependent clock. Under price $p(t)$, cumulative requests at time $t$ equal $N(\int_0^t\lambda(p(s);\theta^*)\,ds)$. The market of size $n$ has stock $nx$ and rate $n\lambda$. Sales stop when stock runs out. The deterministic relaxation $J_n^D$ is the best integrated rate revenue over measurable price paths satisfying the expected-demand stock constraint, with the same scaling. The policy revenue $J_n^\pi$ is its expected sales revenue, and its relative regret is $R_n^\pi=1-J_n^\pi/J_n^D$. Fact 1 states $J_n^D=nJ^D$ and gives a positive uniform lower bound on $J^D$.

Assumption 2 selects $k$ distinct ordinary test prices. Their mean rates identify the parameter through a Lipschitz inverse map $g$, and demand changes at most $\overline K_2\|\theta-\theta'\|_\infty$ as the parameter varies. The square root of each test-price rate is differentiable on $\Theta$. Algorithm 2 spends $\tau_n$ time units testing these prices in equal subintervals, estimates each rate from its Poisson count increment, and sets $\widehat\theta=g(\widehat d)$. It then posts $\widehat p=\max\{p^u(\widehat\theta),p^c(\widehat\theta)\}$, where $p^u$ maximizes revenue rate and $p^c$ minimizes the distance of demand to $x/T$. It keeps that price until time $T$ or stock-out. See §5.1–5.2.

Formalization targets

The capstone is the uniform bound in Proposition 3, equation (17). With $\tau_n\asymp n^{-1/3}$, the mission asks for one constant $C>0$, independent of $n$, $\theta^*$, the optimizer choices, and the probability space, such that

$$\forall\theta^*\in\Theta,\qquad R_n^\pi(x,T;\theta^*)\le C\frac{\sqrt{\log n}}{n^{1/3}}\quad(n\ge2).$$

The intermediate quantitative target is equation (A-25), which retains the learning time:

$$R_n^\pi\le\frac{C_3}{m^D}\left(\tau_n+\frac{\sqrt{\log n}}{\sqrt{n\tau_n}}\right),\qquad m^D=m\min\{T,x/M\}.$$

The milestone list also carries Fact 1, the optimal deterministic price path and value from the first assertion of Lemma 1, both Poisson tails of Lemma 2, the pricing-phase revenue bound (A-17), the deterministic stability bounds (A-19), (A-22), and (A-23), and the parameter-estimation bound of Lemma 6. The paper's assertion that the policy is “asymptotically optimal” follows from the displayed regret estimate together with nonnegative regret; the displayed numerical estimate is the formal goal.

What the result provides

A finite-dimensional demand model lets the seller learn from a fixed set of $k$ prices rather than probing an increasingly fine price grid. Proposition 3 quantifies the resulting revenue loss at $O(\sqrt{\log n}\,n^{-1/3})$, compared with the paper's $O(\sqrt{\log n}\,n^{-1/4})$ upper bound for its nonparametric learn-then-price policy. Both guarantees compare actual expected revenue with the full-information deterministic benchmark, including stock-out. These rates are proved in the article; the mission seeks machine-checked Lean proofs of the stated model, auxiliary bounds, and capstone. No such proof is claimed here.

The formalization would also provide reusable interfaces for a unit-rate Poisson counting process, deterministic inventory-constrained revenue optimization, measurable price selectors, and a random price chosen from normalized count observations. The later single-parameter policy in the paper uses related ideas but is a separate mission with different stages and a different rate.

Main difficulty

A rate estimate can be close to the true rate while the selected price changes between two different optimizers: the unconstrained revenue maximizer and the price that matches inventory to expected demand. A bound for only one optimizer does not control the maximum of the two. The learning price is random, and the number of requests in the pricing phase is evaluated at a random Poisson clock. Stock-out further couples the learning phase to the amount available for later sales. These features prevent a direct substitution of an ordinary parameter-estimation bound into the final revenue formula.

Formalization scope

Lean uses $\mathrm{Fin}(k)\to\mathbb R$ with its sup norm for parameter vectors, a finite positive off price, and a Poisson process on an arbitrary probability space. Each demand curve is defined on all real prices but is constrained on $[\underline p,\overline p]$ and at $p_\infty$; the inverse and concavity conditions apply on the attainable rate interval. The deterministic benchmark is a real supremum over measurable, integrable admissible price paths. The class assumptions make its value nonempty and bounded. Policy revenue uses a nonnegative integral of pathwise revenue, avoiding a default zero from a nonintegrable signed expectation.

Inventory is measured in whole units, so the cap is $\lfloor nx\rfloor$, equal to the paper's $nx$ when that quantity is integral. Test-price observations remain uncapped in the formula for $\widehat d$; if stock runs out during learning, capped later sales are already zero. The continuous optimizer choices are measurable selections satisfying the actual max/min properties for every member of $\Theta$. The bound is uniform over these choices and over all unit-rate Poisson processes.

The printed Assumption 2(i)b asks for a solution to the test-rate equations for every vector in $\mathbb R^k$. Such a solution cannot always lie in compact $\Theta$, although the proof applies Assumption 2(ii) to $\widehat\theta$. Here $g$ is a Lipschitz map into $\Theta$ that recovers each true parameter from its test-rate vector; it can be viewed as the unconstrained inverse followed by a nonexpansive projection in the paper's box example. This explicit convention is required to make the estimate and subsequent use of Assumption 2(ii) coherent. It is an interpretive repair of the printed condition.

The paper prints the regret bound for $n\ge1$, where $\sqrt{\log1}=0$. The exploration policy can lose revenue at $n=1$, so the formal theorem starts at $n\ge2$. The comparison $\tau_n\asymp n^{-1/3}$ is encoded by positive lower and upper multipliers after a fixed threshold, with $0<\tau_n\le T$ for all relevant market sizes. This admits the usual finite initial adjustments and leaves the bound uniform over the sequence. No fixed demand curve, known parameter, finite price grid, or uncapped sales model can satisfy this target by substitution.

Selected references

• Omar Besbes and Assaf Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009, authors' final manuscript revised December 16, 2007. DOI: 10.1287/opre.1080.0640.

Motivation

Most stochastic programs of practical size, such as two-stage recourse models in energy, finance or supply-chain planning, cannot be solved exactly: the expectation in the objective is a high-dimensional integral. The standard remedy is sample average approximation (SAA): replace the expectation by an average over a Monte Carlo sample and solve the resulting deterministic problem. This produces a candidate solution $\hat x$ but says nothing about how good it is. A decision maker needs a statistical certificate: an interval that contains the candidate's optimality gap with a prescribed probability.

Mak, Morton and Wood (Oper. Res. Lett. 24, 1999) built such a certificate from $n_g\ge 30$ independent SAA replications, which requires solving at least 30 optimization problems. Bayraksan and Morton (preprint January 2005, published in Math. Program. 108, 2006) showed that a single replication suffices asymptotically, and gave two variants that use two replications. This mission formalizes their validity theorems.

Setting

Let $\tilde\xi$ be a random vector with distribution $\mu$ on a measurable space $\Xi$, let $X\subseteq\mathbb R^d$ be a set of decisions, and let $f:\mathbb R^d\times\Xi\to\mathbb R$ be a cost. The stochastic program is

$$z^*=\min_{x\in X} Ef(x,\tilde\xi). \qquad\text{(SP)}$$

Its optimal set is $X^*$, and the optimality gap of a candidate $\hat x\in X$ is $\mu_{\hat x}=Ef(\hat x,\tilde\xi)-z^*\ge 0$. The paper assumes throughout:

• (A1) $f(\cdot,\tilde\xi)$ is continuous on $X$, with probability one;
• (A2) $E\sup_{x\in X} f^2(x,\tilde\xi)<\infty$;
• (A3) $X$ is nonempty and compact.

Let $\tilde\xi^1,\tilde\xi^2,\dots$ be i.i.d. copies of $\tilde\xi$, and write $\bar f_n(x)=\frac1n\sum_{i=1}^n f(x,\tilde\xi^i)$. The SAA problem is $z_n^*=\min_{x\in X}\bar f_n(x)$ (SP$_n$), with an optimal solution $x_n^*$. The gap estimator is $G_n(\hat x)=\bar f_n(\hat x)-z_n^*$ (display (2)), and the sample variance of the differences $f(\hat x,\tilde\xi^i)-f(x,\tilde\xi^i)$ is

$$s_n^2(x)=\frac1{n-1}\sum_{i=1}^n\Big[\big(f(\hat x,\tilde\xi^i)-f(x,\tilde\xi^i)\big)-\big(\bar f_n(\hat x)-\bar f_n(x)\big)\Big]^2,$$

with population counterpart $\sigma^2_{\hat x}(x)=\operatorname{var}[f(\hat x,\tilde\xi)-f(x,\tilde\xi)]$. Finally $z_\alpha$ is defined by $P(N(0,1)\le z_\alpha)=1-\alpha$.

The single replication procedure (SRP) solves (SP$_n$) once and reports the one-sided interval $\big[0,\ G_n(\hat x)+z_\alpha s_n(x_n^*)/\sqrt n\big]$ (display (5)). The I2RP takes the variance from a second, independent sample $\tilde\xi^{n+1},\dots,\tilde\xi^{2n}$ and its own minimizer $x_n^{2*}$. The A2RP runs the SRP on both halves of a sample of size $2n$, averages the gaps and the variances as in (10), and scales by $\sqrt{2n}$.

Formalization targets

Goal: Theorem 2 (p. 7)

Under (A1)–(A3), for $\hat x\in X$ and $0<\alpha<1$, provided $\alpha\le1/2$ or $\sigma^2_{\hat x}(x^*_{\max})>0$ (see Formalization scope),

$$\liminf_{n\to\infty}P\left(\mu_{\hat x}\le G_n(\hat x)+\frac{z_\alpha s_n(x_n^*)}{\sqrt n}\right)\ge 1-\alpha. \qquad(6)$$

Consistency (Proposition 1, p. 6)

The milestones follow the paper's own proof:

1. the uniform strong law $\sup_{x\in X}|\bar f_n(x)-Ef(x,\tilde\xi)|\to 0$ w.p.1;
2. (i) $z_n^*\to z^*$ w.p.1;
3. (ii) every limit point of $\{x_n^*\}$ lies in $X^*$ w.p.1;
4. the uniform convergence $s_n^2\to\sigma^2_{\hat x}$ on $X$ w.p.1;
5. (iii) $\sigma^2_{\hat x}(x^*_{\min})\le\liminf_n s_n^2(x_n^*)\le\limsup_n s_n^2(x_n^*)\le\sigma^2_{\hat x}(x^*_{\max})$ w.p.1, where $x^*_{\min}$ and $x^*_{\max}$ minimize and maximize $\sigma^2_{\hat x}$ over $X^*$;
6. the $\varepsilon$-bound of the proof of Theorem 2: if $\alpha\le 1/2$ and $\sigma^2_{\hat x}(x^*_{\min})>0$, then for $0<\varepsilon<1$ the liminf in (6) is at least $\Phi((1-\varepsilon)z_\alpha)$.

Companions

Theorem 3 (p. 9) and Theorem 4 (p. 10) are the same coverage statement for the I2RP and the A2RP. Three further statements are included: the negative bias $Ez_n^*\le z^*$ of display (1), the pathwise bound $G_n(\hat x)\ge\bar f_n(\hat x)-\bar f_n(x)$ for $x\in X$, and the consistency $\liminf_n s_n'^2\ge\sigma^2_{\hat x}(x^*_{\min})$ of the pooled variance.

Significance

Theorem 2 makes a single SAA solve enough for an asymptotically valid upper confidence bound on the optimality gap. It cuts the computational cost of the multiple-replication procedure by a factor of about thirty, and it needs no asymptotic normality of $G_n(\hat x)$, which typically fails when (SP) has several optimal solutions. The two-replication variants lessen the small-sample under-coverage of the SRP. The single- and two-replication estimators were later reused in sequential sampling procedures for SAA.

As far as is known, none of these results has been machine-checked. A complete formalization needs a uniform strong law of large numbers over a compact parameter set, which is a reusable result in its own right, together with the SAA consistency theory and a central-limit argument for a statistic that is not itself asymptotically normal.

Difficulty

The obvious route would be to show that $G_n(\hat x)$ is asymptotically normal and apply a standard confidence-interval argument. That fails: $z_n^*$ is a minimum of sample averages, and when $X^*$ is not a singleton its limit law is the law of a minimum of correlated Gaussians, not a Gaussian. The paper's argument has to bound the coverage from below without that limit law. It also needs to control the sample variance at a random, non-convergent minimizer $x_n^*$, which only accumulates on $X^*$. The uniform strong law (Rubinstein–Shapiro, Lemma A1) on which both consistency statements rest is not in Mathlib.

Formalization scope

The Lean development uses these conventions:

• Decisions live in EuclideanSpace ℝ (Fin d). The paper's $\mathbb R^n$ is renamed $\mathbb R^d$ because $n$ is the sample size.
• $\mu$ is a probability measure on $\Xi$ (the law of $\tilde\xi$), and $Ef(x,\tilde\xi)$ is the Bochner integral $\int f(x,\cdot)\,d\mu$.
• The sample is one infinite i.i.d. sequence ξ : ℕ → Ω → Ξ on a probability space $(\Omega,P)$, 0-based: $\tilde\xi^i$ is ξ (i-1). The second sample of Theorems 3–4 is ξ n, …, ξ (2n-1), exactly as printed, and the A2RP's "random" partition is this fixed one, which has the same joint law.
• Estimators are functions of a sample path. $z^*$ and $z_n^*$ are infima of images of $X$, and $X^*$ is an argmin set.
• Probabilities are ℝ≥0∞-valued, so the liminf in (6) is genuine. Proposition 1 (iii) is stated in its equivalent $\varepsilon$-form, which avoids real liminf/limsup junk values.
• $z_\alpha$ is any real with cdf (gaussianReal 0 1) zα = 1 - α.

Standing assumptions and pins. Every goal-level statement carries (A1)–(A3) and the i.i.d. hypothesis. Three hypotheses are made explicit that the paper leaves implicit:

1. $f(x,\cdot)$ is measurable for each $x$ ("$f(x,\tilde\xi)$ is a random variable");
2. $x_n^*$ is a measurable map that, almost surely, lies in $X$ and minimizes $\bar f_n$ over $X$ on the same sample;
3. (A2) is read as "$\sup_{x\in X}f^2(x,\cdot)$ has an integrable majorant", which avoids proving that the supremum is measurable.

At $n\le 1$ the factors $1/n$, $1/(n-1)$ and $1/\sqrt n$ evaluate to Lean's $0$; every coverage statement is a liminf and ignores them.

Several encodings would trivialize the statement, and all are ruled out. The minimizer $x_n^*$ must minimize the SAA problem of its own sample: a free $x_n^*$, or one fitted to the other sample, would change the theorem. The second sample must not be replaced by an independent sequence. The quantile must not be pinned through an sInf. Positivity of $\sigma^2_{\hat x}(x^*_{\min})$ is a hypothesis only of the $\varepsilon$-bound, as on p. 8.

One correction of the paper. Theorems 2 and 4 are stated for every $0<\alpha<1$, but for $\alpha>1/2$ the paper's argument (replace $x^*_{\min}$ by $x^*_{\max}$) needs $\sigma^2_{\hat x}(x^*_{\max})>0$, and without it both statements are false: for $X=[-1,1]$, $f(x,\xi)=x^2-2x\xi$, $\tilde\xi\sim N(0,1)$, $\hat x=0$ and $\alpha=0.9$, the SRP coverage tends to about $0.010$ and the A2RP coverage to $e^{-2z_\alpha^2}\approx0.037$, both below $0.1$. The Lean goal and Theorem 4 therefore carry the hypothesis "$\alpha\le1/2$, or $\sigma^2_{\hat x}(x)>0$ for some $x\in X^*$". Theorem 3 is stated as printed.

Contributions are welcome at every level. The most reusable one is the uniform strong law of large numbers for Carathéodory integrands on a compact set with an integrable envelope, which also serves other SAA consistency results.

Selected references

• G. Bayraksan, D. P. Morton, Assessing Solution Quality in Stochastic Programs, preprint (January 26, 2005); published in Math. Program. 108 (2006). https://doi.org/10.1007/s10107-006-0720-x
• W. K. Mak, D. P. Morton, R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Oper. Res. Lett. 24 (1999) 47–56. https://doi.org/10.1016/S0167-6377(98)00054-6
• R. Y. Rubinstein, A. Shapiro, Discrete Event Systems: Sensitivity Analysis and Stochastic Optimization by the Score Function Method, Wiley, 1993 (Lemma A1, p. 67; Theorem A1, p. 69).
• A. Shapiro, Monte Carlo sampling methods, in: Handbooks in OR & MS 10, Stochastic Programming, Elsevier, 2003, 353–425. https://doi.org/10.1016/S0927-0507(03)10006-0

Motivation

Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate $O(1/\sqrt n)$ for non-strongly-convex objectives, and $O(1/(\mu n))$ when the objective is $\mu$-strongly convex. For least squares, $\mu$ is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.

F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate $O(1/n)$ with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.

Setting

Let $\mathcal H=\mathbb R^d$ with $d\ge1$, inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For $a\in\mathcal H$, $a\otimes a$ is the operator $b\mapsto\langle a,b\rangle a$. For self-adjoint operators, $A\preccurlyeq B$ means that $B-A$ is positive semi-definite.

The data are independent and identically distributed pairs $(x_n,z_n)\in\mathcal H\times\mathcal H$, $n\ge1$, with finite second moments. The covariance operator is $H=\mathbb E[x_n\otimes x_n]$, assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective

$$f(\theta)=\tfrac12\,\mathbb E\big[\langle\theta,x_n\rangle^2-2\langle\theta,z_n\rangle\big]$$

attains its global minimum at $\theta^*$, and $\xi_n=z_n-\langle\theta^*,x_n\rangle x_n$ is the residual. The model need not be well specified: $\mathbb E[\xi_n\mid x_n]$ need not vanish. Two constants $R,\sigma>0$ satisfy

$$\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq\sigma^2H,\qquad \mathbb E\big[\|x_n\|^2x_n\otimes x_n\big]\preccurlyeq R^2H .$$

These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size $\gamma$, started at $\theta_0\in\mathcal H$, is

$$\theta_n=\theta_{n-1}-\gamma\big(\langle\theta_{n-1},x_n\rangle x_n-z_n\big)=(I-\gamma x_n\otimes x_n)\theta_{n-1}+\gamma z_n ,$$

and its average is $\bar\theta_{n-1}=n^{-1}\sum_{k=0}^{n-1}\theta_k$.

Formalization targets

Goal: Theorem 1, Eq. (2)

For every step size $0<\gamma<1/R^2$ and every $n\ge1$,

$$\mathbb E\big[f(\bar\theta_{n-1})-f(\theta^*)\big]\le\frac{1}{2n}\left[\frac{\sigma\sqrt d}{1-\sqrt{\gamma R^2}}+R\|\theta_0-\theta^*\|\frac{1}{\sqrt{\gamma R^2}}\right]^2 .$$

The constants are the paper's. A companion item states the case $\gamma=1/(4R^2)$, where the bound reads $\frac2n\big[\sigma\sqrt d+R\|\theta_0-\theta^*\|\big]^2$.

Milestones (Appendix A)

1. The excess risk is a quadratic form: $f(\theta)-f(\theta^*)=\tfrac12\langle\theta-\theta^*,H(\theta-\theta^*)\rangle$.
2. Consequences of (A6): $\mathbb E\|x_n\|^2\le R^2$, $\operatorname{tr}H\le R^2$, $H\preccurlyeq R^2I$, and $\gamma H\preccurlyeq I$ for $\gamma\le1/R^2$.
3. Lemma 1: for a recursion $\alpha_n=(I-\gamma x_n\otimes x_n)\alpha_{n-1}+\gamma\xi_n$ with martingale-difference noise and $\gamma R^2\le1$,

$$(1-\gamma R^2)\,\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle+\tfrac{1}{2n\gamma}\mathbb E\|\alpha_n\|^2\le\tfrac{1}{2n\gamma}\|\alpha_0\|^2+\tfrac{\gamma}{n}\textstyle\sum_{k=1}^{n}\mathbb E\|\xi_k\|^2 .$$

4. Lemma 3: $(1-(1-u)^n)^2\le nu$ for $u\in[0,1]$ and $n>0$.
5. Lemma 2: for $\alpha_n=(I-\gamma H)\alpha_{n-1}+\gamma\xi_n$ with $\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq C$, the second-moment bound (13) and

$$\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle\le\tfrac{1}{n\gamma}\|\alpha_0\|^2+\tfrac1n\operatorname{tr}(CH^{-1}).$$

6. The pathwise decomposition $\theta_n-\theta^*=M^n_1(\theta_0-\theta^*)+\gamma\sum_{k=1}^nM^n_{k+1}\xi_k$ (A.2).
7. The initial-condition bound $\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\le\|\eta_0\|^2/(n\gamma)$ for the noise-free process (A.3).
8. The expansion of the noise process (A.4): the remainder recursion (16), the covariance bound (17) $\mathbb E[\eta^r_{n-1}\otimes\eta^r_{n-1}]\preccurlyeq\gamma^{r+1}R^{2r}\sigma^2I$, the order-$r$ bound $\frac1n\gamma^rR^{2r}d\sigma^2$, the remainder bound $\frac{\gamma^{r+2}\sigma^2R^{2r+4}}{1-\gamma R^2}$, and the noise bound

$$\big(\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\big)^{1/2}\le\frac{\sigma\sqrt d}{\sqrt n}\cdot\frac{1}{1-\sqrt{\gamma R^2}}\quad(\eta_0=0,\ \gamma R^2<1).$$

Significance

The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term $\sigma^2d/n$, which matches the minimax rate for least-squares regression, and a bias term $R^2\|\theta_0-\theta^*\|^2/(\gamma n)$. Neither involves the smallest eigenvalue of $H$, so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in $\mathbb R^d$, second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator $H$, so they apply beyond this model. The mission also records the corrections the appendix needs (an "$=$" that should be "$\preccurlyeq$" in (13), an index in (16), and the exponent of $\|\eta_0\|$ in A.5).

Difficulty

Two steps resist the naive approach. First, the obvious one-step analysis — expand $\|\theta_n-\theta^*\|^2$ and take expectations — yields the bias part and Lemma 1, but on the noise it gives only $\gamma\sum_k\mathbb E\|\xi_k\|^2/n$, which does not decrease with $n$. The $\sigma^2d/n$ rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with $x_n\otimes x_n$ replaced by its mean $H$. The random recursion is therefore expanded in powers of $\gamma$ around the mean recursion, and each term $\eta^r$ needs its own covariance bound, by induction on $r$, using the independence of $x_n$ from $\eta^{r}_{n-1}$. Second, the induction relies on Loewner-order bookkeeping: sums of $(I-\gamma H)^{2k}H$ must be bounded uniformly in $n$ without dividing by small eigenvalues.

Formalization scope

The space $\mathcal H$ is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and $H^{-1}$ is an explicit two-sided inverse. Observations are indexed from $1$. Averages are $\bar p_{n-1}=n^{-1}\sum_{k=0}^{n-1}p_k$, with $n\ge1$ in every statement that uses them. The covariance operator is defined by its bilinear form, $\langle v,Hw\rangle=\mathbb E[\langle x_1,v\rangle\langle x_1,w\rangle]$. Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example $\mathbb E\langle\xi_1,v\rangle^2\le\sigma^2\langle v,Hv\rangle$ for all $v$), which is the same order for self-adjoint operators.

Lean's Bochner integral is $0$ on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed $x_n$ would satisfy (A6) vacuously and a conclusion could hold through the value $0$; neither formalization is acceptable. Independence is of the pairs $(x_n,z_n)$, not of $x_n$ and $z_n$ separately. (A4) is attainment of the minimum, not a gradient condition.

The following hypotheses are added to the page and disclosed in each item:

• $\gamma>0$ (a step size, and $\sqrt{\gamma R^2}$ is a denominator);
• $n\ge1$;
• the positivity and self-adjointness of $H$ in Lemma 2;
• $\gamma R^2<1$ instead of $\le1$ in the remainder bound, which divides by $1-\gamma R^2$.

A complete development needs:

• conditional expectations of $\mathbb R^d$-valued martingale differences, and the orthogonality of their sums;
• independence of a fresh observation from the past iterates;
• spectral calculus for $(I-\gamma H)^k$;
• Minkowski's inequality in $L^2$.

All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.

Selected references

• F. Bach and E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), Advances in Neural Information Processing Systems 26, 2013. https://arxiv.org/abs/1306.2119
• B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046
• R. Aguech, E. Moulines and P. Priouret, On a perturbation approach for the analysis of stochastic tracking algorithms, SIAM Journal on Control and Optimization 39(3), 2000. https://doi.org/10.1137/S0363012997331639
• F. Bach and E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, Advances in Neural Information Processing Systems 24, 2011. https://hal.science/hal-00608041

Motivation

A firm that sets prices without knowing how demand responds to them has to learn the demand curve from its own sales. Each price it charges is both a revenue decision and an experiment. The natural policy, certainty equivalent pricing, re-estimates the demand parameters after every period and charges the price that would be optimal if the estimates were exact. den Boer and Zwart show that this policy can fail: with positive probability its prices settle at a suboptimal value, because they converge too fast for the estimates to keep improving (den Boer–Zwart 2014, Proposition 1, the subject of the companion mission). The same phenomenon was found by Lai and Robbins (1982) for a linear control problem.

Their remedy, Controlled Variance Pricing (CVP), keeps certainty equivalent pricing but forces the sample variance of the chosen prices to decay no faster than $t^{\alpha-1}$. The main result is that this small amount of enforced exploration gives regret $O(T^\alpha + T^{1-\alpha}\log T)$, hence $O(T^{1/2+\delta})$ for every $\delta > 0$, for a broad class of demand models that are specified only through their first two moments. Keskin and Zeevi (2014) later placed CVP in a larger family of semi-myopic policies with $\sqrt T\log T$ regret for linear demand.

Setting

A seller chooses in each period $t = 1, 2, \dots$ a price $p_t \in [p_l, p_h]$, with $0 < p_l < p_h$, and then observes demand $d_t$. Demand at price $p$ has mean $h(a_0^{(0)} + a_1^{(0)}p)$ and variance $\sigma^2 v(h(a_0^{(0)} + a_1^{(0)}p))$, where the link $h$ and variance function $v$ are known and $C^2$ on $[0,\infty)$, $\dot h > 0$, and the parameter $a^{(0)} = (a_0^{(0)}, a_1^{(0)})$ with $a_0^{(0)} > 0 > a_1^{(0)}$ is unknown. The noise $e_t = d_t - h(a_0^{(0)} + a_1^{(0)}p_t)$ is a martingale difference with conditional variance $\sigma^2 v(\cdot)$ and a uniformly bounded conditional moment of some order $r > 3$.

The expected revenue is $r(p, a) = p\,h(a_0 + a_1p)$. Near $a^{(0)}$ it has a unique maximizer $p(a)$ in the open interval $(p_l, p_h)$ with $\partial_p^2 r < 0$ there, and $p_{\mathrm{opt}} = p(a^{(0)})$. The regret of a policy is

$$\operatorname{Regret}(T) = \mathbb E\Big[\sum_{t=1}^T r(p_{\mathrm{opt}}, a^{(0)}) - r(p_t, a^{(0)})\Big].$$

The estimate $\hat a_t$ is the maximum quasi-likelihood estimate (MQLE), the root of the quasi-score equation (3), $\sum_{i\le t} \frac{\dot h}{\sigma^2 v(h)}(1, p_i)^\top(d_i - h(\hat a_0 + \hat a_1 p_i)) = 0$. With $\bar p_t$ and $\operatorname{Var}(p)_t$ the sample mean and variance of $p_1,\dots,p_t$, the taboo interval is $\mathrm{TI}(t) = (\bar p_t - w_t, \bar p_t + w_t)$ with $w_t = \sqrt{c[(t+1)^\alpha - t^\alpha](t+1)/t}$. CVP starts from two distinct prices $p_1, p_2$, fixes $\alpha \in (0,1)$ and $0 < c < 2^{-\alpha}(p_1-p_2)^2\min\{1,(3\alpha)^{-1}\}$, and for $t \ge 2$: if $\hat a_t$ does not exist or has the wrong signs, it charges whichever of $p_1, p_2$ is farther from $\bar p_t$; otherwise it charges $p(\hat a_t)$ if that keeps $\operatorname{Var}(p)_{t+1} \ge c(t+1)^{\alpha-1}$, and the best price outside $\mathrm{TI}(t)$ if not.

Formalization targets

Goal: Theorem 1

$$\operatorname{Regret}(T, \mathrm{CVP}) = O\big(T^\alpha + T^{1-\alpha}\log T\big) \qquad (1/2 < \alpha < 1),$$

stated as: there is $K > 0$, depending on the model, $\alpha$, $c$ and the initial prices but not on $T$, with $\operatorname{Regret}(T) \le K(T^\alpha + T^{1-\alpha}\log T)$ for all $T \ge 1$. The constant is left free, so the statement survives any sharpening of the constants.

Milestones

1. Proposition 2: $\operatorname{Var}(p)_t \ge c\,t^{\alpha-1}$ for all $t \ge 2$ along every CVP path.
2. Lemma 1: $\lambda_{\max}(P_t) \le (1+p_h^2)t$ and $t\operatorname{Var}(p)_t \le (1+p_h^2)\lambda_{\min}(P_t)$ for the design matrix $P_t = \sum_{i\le t}(1,p_i)^\top(1,p_i)$.
3. Proposition 3: $\hat a_t$ eventually exists, $\hat a_t \to a^{(0)}$ a.s., and for some $\rho_0$, $\mathbb E[T_{\rho_0}^{1/2}] < \infty$ and $\mathbb E[\|\hat a_t - a^{(0)}\|^2\mathbf 1_{t > T_{\rho_0}}] = O(\log t/t^\alpha)$.
4. Eq. (11): in the normal–linear case, $\mathbb E\|\hat a_t - a^{(0)}\|^2 = O(\log t / t^\alpha)$.
5. Eqs. (17), (18), (20): the quadratic revenue gap, the local Lipschitz bound on $p(a)$, and $|p_{t+1} - p(\hat a_t)| \le |\mathrm{TI}(t)|$ for large $t$.
6. The closing bound $\mathbb E[(p_t - p_{\mathrm{opt}})^2] = O(t^{\alpha-1} + \log t/t^\alpha)$.

Significance

The theorem shows that a policy that is certainty equivalent almost all of the time, with a single interpretable tuning parameter $\alpha$, attains regret $O(T^{1/2+\delta})$ in generalized linear demand models, without distributional assumptions beyond two moments. It explains the role of $\alpha$ precisely: $T^\alpha$ is the cost of exploration and $T^{1-\alpha}\log T$ the cost of estimation error. Proposition 2 and Lemma 1 are reusable for any policy that enforces a variance floor on its actions, and (11) is a self-contained rate for least squares under adaptively chosen designs.

The result is proved in the paper, with Proposition 3 delegated to den Boer and Zwart (2012) for general links. To our knowledge none of it has been machine-checked. A formalization would verify the delegated consistency argument, fix the conditions under which it applies (see Formalization scope), and provide a Lean development of adaptive least squares and quasi-likelihood rates that the related Keskin–Zeevi missions also need.

Difficulty

The deterministic parts are short. The difficulty is Proposition 3. The prices are chosen adaptively from past data, so the regressors are not independent of the noise, and standard rates for (quasi-)likelihood estimates do not apply. The natural argument, bounding $\|\hat a_t - a^{(0)}\|^2$ by $Q_t/\lambda_{\min}(P_t)$ with $Q_t$ a self-normalized martingale quadratic form, needs a bound $\mathbb E[Q_t] = O(\log t)$ that holds in expectation and not only almost surely, as in Lai and Wei (1982). For a non-linear link the MQLE is defined only implicitly, and its existence near $a^{(0)}$ has to be shown first, with a moment bound on the last time it fails. That is the random time $T_\rho$. Turning almost-sure consistency into a rate in expectation is where most of the work lies.

Formalization scope

All declarations live in the namespace CVPricing.Regret. Periods are 1-based. Prices, demands and parameters are real; $a = (a_0, a_1) \in \mathbb R \times \mathbb R$ with the Euclidean norm (euclidNorm), not Mathlib's sup norm. The design matrix, sample mean and $t\operatorname{Var}(p)_t$ are the published Keskin–Zeevi definitions fisherOf, avgPriceOf, infoMetricOf. Every $O(\cdot)$ is "there is $K > 0$ such that for all $t$", with $K$ quantified after the model data. Rates are stated for $t \ge 2$ and the regret for $T \ge 1$. $h$ and $v$ are total functions constrained on $[0,\infty)$. A root of (3) counts only where $\hat a_0 + \hat a_1 p_i \ge 0$ for every observed $p_i$. CVP is a predicate on a realized path that allows every maximizer in (7) and (8).

Disclosed deviations from the page:

• the model requires $a_0^{(0)} + a_1^{(0)}p_h > 0$ (printed: $\ge 0$), because in the boundary case the policy's case (c) fires infinitely often and the proof of Theorem 1 does not cover it;
• (3) is assumed to have at most one root (the page notes roots need not be unique, and the policy cannot select the root nearest $a^{(0)}$);
• the neighbourhood assumption is read as a unique maximizer over $[p_l, p_h]$ lying in $(p_l, p_h)$;
• the demand process is given by its conditional mean, its conditional variance and (2), with integrable noise moments, not by a fixed law $D(p)$;
• the initial prices are deterministic.

Corrected slips: Proposition 2 is stated for $c \le 2^{-\alpha}(p_1-p_2)^2\min\{1/2,(3\alpha)^{-1}\}$, because the printed range fails at $t=2$ ($\operatorname{Var}(p)_2 = (p_1-p_2)^2/4$, not $/2$). Theorem 1 keeps the printed range. Eq. (20) is stated for $p_{t+1}$ and for $t$ beyond an explicit threshold.

The goal does not assume the variance bound, consistency or (20). The policy contains the variance check and the taboo interval, and the regret is the expectation over the actual price process. A statement that assumed any of these, or that dropped the taboo step, would be trivial or false. Contributions are welcome on adaptive least squares (Sherman–Morrison and determinant-ratio bounds), martingale last-time moment bounds, and the implicit-function step (18).

Selected references

• A. V. den Boer, 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
• A. V. den Boer, B. Zwart, Mean square convergence rates for maximum quasi-likelihood estimators, Stochastic Systems 4(2):375–403, 2014 (cited as 2012 working paper). https://doi.org/10.1214/12-SSY086
• T. L. Lai, C. Z. Wei, Least squares estimates in stochastic regression models with applications to identification and control of dynamic systems, Annals of Statistics 10(1):154–166, 1982. https://doi.org/10.1214/aos/1176345697
• T. L. Lai, H. Robbins, Iterated least squares in multiperiod control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/S0196-8858(82)80005-5
• N. B. Keskin, 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