All missions

Motivation

A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).

The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.

Timeline:

• 2004: Talluri and van Ryzin prove revenue-ordered assortments optimal under the multinomial logit model.
• 2014: Rusmevichientong et al. show NP-hardness of the assortment problem for mixtures of logits, and prove that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit models.
• 2016–2019: Berbeglia and Joret prove the guarantees $1/k$ and $1/(1+\ln(r_k/r_1))$ under any regular choice model and show them tight (arXiv v1 2016, v3 2019; Algorithmica 2020). Aouad, Farias, Levi and Segev (2018) show that under random utility models no efficient algorithm does essentially better than these ratios.

Setting

There is a finite nonempty set $\mathcal C$ of products. For a choice set $S\subseteq\mathcal C$, $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys product $x$, and $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ is the probability that the customer buys nothing. The system $\mathcal P$ is a regular discrete choice model if

1. $\mathcal P(x,S)\ge0$ for every $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ whenever $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.

Each product has a positive price $r(x)>0$. The revenue of $S$ is $\operatorname{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\operatorname{rev}(S)$. Let $0<r_1<\cdots<r_k$ be the distinct prices, so $k$ counts price levels and not products, and set $r_0=0$. The revenue-ordered assortments are $S_i=\{x\in\mathcal C : r(x)\ge r_i\}$, $i=1,\dots,k$, and the heuristic earns

$$\mathrm{RO}=\max_{1\le i\le k}\operatorname{rev}(S_i).$$

Formalization targets

Goal: Theorem 3.2

$$\mathrm{OPT}\;\le\;\Big(\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\Big)\,\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\;\le\;1+\ln\frac{r_k}{r_1}.$$

The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).

Milestones

• Lemma 2.1: $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• Inequality (5): $\operatorname{rev}(S_i)\ge r_i\sum_{x\in S^*\cap S_i}\mathcal P(x,S^*)$ for every $S^*$ and $i\in[k]$.
• Theorem 3.1: $\mathrm{OPT}\le k\cdot\mathrm{RO}$.
• Rearrangement (proof of Theorem 3.2): $\operatorname{rev}(S^*)=\sum_{\ell}(r_\ell-r_{\ell-1})\sum_{x\in S^*\cap S_\ell}\mathcal P(x,S^*)$, and $\operatorname{rev}(S^*)\le\sum_\ell\frac{r_\ell-r_{\ell-1}}{r_\ell}\operatorname{rev}(S_\ell)$.
• Logarithmic bound: $\sum_{\ell=1}^k\frac{a_\ell-a_{\ell-1}}{a_\ell}\le1+\ln(a_k/a_1)$ for $0=a_0<a_1<\cdots<a_k$.

Significance

The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of $k$ or of $r_k/r_1$, that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.

Difficulty

The argument is short, but two points are easy to get wrong. First, revenues of $S_i$ and of an optimal $S^*$ involve choice probabilities evaluated at different sets, so the comparison must pass through $S^*\cap S_i$, using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention $r_0=0$; indexing by products or dropping $r_0$ gives a different quantity. The comparison of the sum with $\ln(r_k/r_1)$ is a Riemann-sum estimate for $\int dt/t$ and needs a real-analysis lemma not phrased this way in Mathlib.

Formalization scope

• Products are a finite nonempty type C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.
• IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.
• r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is $\operatorname{rev}(S)$ and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.
• Price levels are 1-based: level r i is $r_i$ for $1\le i\le k$ and level r 0 = 0; numVals r is $k$, the number of distinct values. roSet r i is $S_i$; roValue P r is the maximum over $i\in\{1,\dots,k\}$ only.
• Approximation guarantees are stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. $\ln$ is Real.log, applied to $r_k/r_1\ge1$.
• Ruled out: a maximum over all subsets in place of $\mathrm{RO}$ (which makes the bound trivial), a regularity axiom without its no-purchase case, the logarithmic form alone in place of the sum form, and any specific choice model (logit, Markov chain, random utility) in place of an arbitrary regular $\mathcal P$.

Needed infrastructure: finite sums over price levels and summation by parts, the comparison of $(b-a)/b$ with $\ln(b/a)$, and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Why the shape of the optimal pricing policy matters

A retailer holding a fixed stock of a perishable or seasonal good (fashion items, airline seats, hotel rooms, concert tickets) must sell it before a deadline, after which unsold units are worthless. Demand is random and depends on the posted price, and the firm may change its price at any time. Dynamic pricing asks how the price should depend on the remaining stock and the remaining time.

Gallego and van Ryzin (Management Science 40(8), 1994) posed this problem as a continuous-time intensity control problem and established its basic structure. Their Theorem 1 says that the optimal expected revenue is strictly increasing and strictly concave in both the stock and the time remaining, and that the optimal price falls as stock grows and rises with the time left to sell. The paper is a standard reference of revenue management; the structural result is the continuous-time counterpart of the monotonicity of marginal values in discrete-time models (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 5.2), and it is what makes the optimal policy computable by restricting attention to monotone policies. The paper credits a slightly weaker version to Kincaid and Darling (1963). The source formalized here is the published 1994 article.

The model and the Hamilton–Jacobi system

The firm chooses a demand rate $\lambda$ from a set $\Lambda \subseteq [0,\infty)$ of allowable rates, an interval containing $0$; the market then sets the price $p(\lambda)$, where $p$ is the inverse demand function, strictly decreasing and nonnegative on the positive rates. The rate $0$ corresponds to the null price at which nothing sells. The revenue rate is

$$r(\lambda) = \lambda\,p(\lambda), \qquad r(0) = 0.$$

The demand function is regular when $r$ is continuous, bounded and concave on $\Lambda$ and has a least maximizer $\lambda^* = \min\{\lambda : r(\lambda) = \max_{\mu\in\Lambda} r(\mu)\}$. The exponential demand $\lambda(p) = ae^{-p}$, with $\Lambda=[0,a]$, $p(\lambda)=\log(a/\lambda)$ and $\lambda^*=a/e$, is the running example.

With $n$ units in stock and time remaining $t$, write $J(n,t)$ for the optimal expected revenue. The paper derives the Hamilton–Jacobi system

$$\frac{\partial J(n,t)}{\partial t} = \sup_{\lambda\in\Lambda}\big[r(\lambda) - \lambda\big(J(n,t)-J(n-1,t)\big)\big], \qquad n\ge1,\ t>0, \tag{8}$$

with $J(n,0)=0$ and $J(0,t)=0$. The difference $J(n,t)-J(n-1,t)$ is the marginal value of an item; a rate attaining the supremum is an optimal intensity $\lambda^*(n,t)$, and $p(\lambda^*(n,t))$ is the optimal price $p^*(n,t)$.

Formalization targets

Goal: Theorem 1 (p. 1005)

For the solution $J$ of (8), with $r$ strictly concave, differentiable on the interior of $\Lambda$, and $\lambda^*$ interior:

$$J(n,t)\ \text{strictly increasing in } n\ (t>0)\ \text{and in } t\ (n\ge1);\qquad J(n+1,t)-J(n,t) < J(n,t)-J(n-1,t);$$ $$t\mapsto J(n,t)\ \text{strictly concave};\qquad \exists\,\lambda^*(n,t):\ \lambda^*\!\uparrow_n,\ \lambda^*\!\downarrow_t,\quad p^*\!\downarrow_n,\ p^*\!\uparrow_t\ \text{(strictly)}.$$

Milestones

1. The supremum in (8) is a maximum over $[0,\lambda^*]$ whenever the marginal value is nonnegative (proof of Proposition 1).
2. Proposition 1: (8) has a unique solution, and $\lambda^*(n,s)\le\lambda^*$.
3. Eq. (26): $J(n,t)-J(n-1,t) = r'(\lambda^*(n,t)) > 0$ for $t>0$.
4. The case $n=1$ of Theorem 1: $\lambda^*(1,t)$ strictly decreasing and $J(1,t)$ strictly concave in $t$.
5. $\lambda^*(n,0^+) = \lambda^*$.
6. Eqs. (9)–(10), exponential demand: $J(n,t) = \log\sum_{i=0}^n(\lambda^*t)^i/i!$ and $p^*(n,t) = J(n,t)-J(n-1,t)+1$.
7. Proposition 3, exponential demand: $\lambda^*(n,t)\le\lambda^D(n,t)=\min\{\lambda^*,n/t\}$ and $p^*(n,t)\ge p(\lambda^D(n,t))$.

Significance

Theorem 1 is the qualitative backbone of single-product dynamic pricing. Concavity of $J$ in $n$ means that each additional unit is worth less than the previous one, which is the basis of bid-price and marginal-value reasoning in revenue management; the monotone price path justifies markdown practice as the deadline approaches and reduces the policy search to monotone policies. Proposition 3 answers, for exponential demand, a question raised by Mills (1959): the stochastic optimal price is never below the deterministic one. The closed form (9)–(10) is one of the few exactly solvable intensity control problems in pricing.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires the comparison and monotonicity theory of a countable system of coupled ordinary differential equations whose right-hand side is a convex conjugate, a theory that Mathlib does not package. A complete development would also certify the corrected hypotheses of Theorem 1 described below.

Difficulty

The value functions are defined only implicitly by (8), a triangular infinite system of ODEs in which each $J(n,\cdot)$ is driven by $J(n-1,\cdot)$ through the nonsmooth map $\Delta\mapsto\sup_\lambda[r(\lambda)-\lambda\Delta]$. Monotonicity of the optimal intensity in $t$ is a statement about the time derivative of a marginal value, and the paper establishes it by an induction on $n$ combined with an argument by contradiction on the first interval where monotonicity could fail. The obvious approach of differentiating (8) twice in $t$ needs second derivatives of $r$ and of $J$ that the hypotheses do not provide, and the paper's own proof of Proposition 1 assumes that $J$ is nondecreasing in $n$, which is only established in Theorem 1; a rigorous development must break this circularity.

Formalization scope

A regular demand function is a Lean structure (GVRPricing.Structure.Model) holding $\Lambda$, $p$ and $\lambda^*$ with the paper's standing assumptions of §2.1: $0\in\Lambda\subseteq[0,\infty)$ an interval, $p$ strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$, $r(\lambda)=\lambda p(\lambda)$ continuous, concave and bounded on $\Lambda$, and $\lambda^*$ the least maximizer. The definition IsHJBSolution encodes (8) for $J:\mathbb N\to\mathbb R\to\mathbb R$, with the second argument the time remaining, the two-sided derivative at each $t>0$, continuity on $[0,\infty)$, the boundary conditions, and the requirement that the set inside the supremum be bounded above, so that the real supremum is never a default value. An optimal intensity at $(n,t)$ is any $\ell\in\Lambda$ maximizing $\lambda\mapsto r(\lambda)-\lambda(J(n,t)-J(n-1,t))$ over $\Lambda$.

All theorems are about solutions of (8), on which the paper's proofs operate. The identification of the solution of (8) with the supremum of expected revenue over non-anticipating pricing policies is Brémaud's verification theorem, which the paper cites and does not prove; it is not part of this mission.

Added hypotheses and corrected statements.

• As printed, Theorem 1 assumes only a regular demand function and is false: for $r(\lambda)=\sqrt\lambda$ on $[0,1]$ and $r=1$ beyond, $\lambda^*(1,t)=1$ for all $t\in(0,\ln2]$; for $r(\lambda)=\lambda-\lambda^2/4$ on $\Lambda=[0,1]$, $\lambda^*=1$ is on the boundary and $\lambda^*(1,t)=1$ for small $t$. The goal, eq. (26) and the case $n=1$ therefore assume that $r$ is strictly concave, differentiable on the interior of $\Lambda$, and that $\lambda^*$ is interior; the appendix proof uses all three. Proposition 1, the restriction lemma and $\lambda^*(n,0^+)=\lambda^*$ use only the printed assumptions.
• Strict claims in $n$ are made for $t>0$, since $J(n,0)=0$ for all $n$; optimal intensities are considered for $n\ge1$, $t>0$.
• Proposition 1's bound "$\lambda^*(n,s)\le\lambda^*$ for $0\le s$" is read at $s=0$ as "$\lambda^*$ is optimal", since every maximizer of $r$ is optimal there.
• Proposition 3 is stated for $n\ge1$, $t>0$ (the page says $n\ge0$, $t\ge0$, where $n/t$ or the optimal intensity is undefined).
• The exponential results use the paper's normalization $\alpha=1$ of $\lambda(p)=ae^{-\alpha p}$.
• The case $n=1$ omits the displayed identities involving $r''$ and $\lambda^{*\prime}$, which presuppose second derivatives; its conclusions are stated.

A formalization that defines $J$ by a formula, or postulates a monotone function as the optimal intensity, would trivialize the goal: the goal quantifies over every solution of (8), and the optimal intensity it asserts must maximize the right-hand side of (8) at every $(n,t)$.

A complete development needs comparison principles for scalar ODEs with Lipschitz right-hand sides, properties of the concave conjugate $\Delta\mapsto\sup_\lambda[r(\lambda)-\lambda\Delta]$ (monotonicity, Lipschitz continuity, envelope theorem), and monotone comparative statics of maximizers. These are reusable well beyond this mission; contributions of any of them, or of the milestones in any order, are welcome.

Selected references

• G. Gallego, 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
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
• W. M. Kincaid, D. A. Darling, An Inventory Pricing Problem, Journal of Mathematical Analysis and Applications 7, 183–208, 1963. https://doi.org/10.1016/0022-247X(63)90047-7
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Motivation

Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.

This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.

Setting

Let $M$ be a finite set of elements. For subsets we write $N + e$ for $N \cup \{e\}$ and $P_1 + P_2$ for $P_1 \cup P_2$.

Rank system. A function $r$ assigning an integer $r(N)$ to each $N \subseteq M$ satisfies the rank postulates if

• $(\mathrm R_1)$ the rank of the null subset is zero;
• $(\mathrm R_2)$ for any subset $N$ and any element $e$ not in $N$, $r(N+e) = r(N) + k$ with $k = 0$ or $1$;
• $(\mathrm R_3)$ for any subset $N$ and elements $e_1, e_2$ not in $N$, if $r(N+e_1) = r(N+e_2) = r(N)$, then $r(N+e_1+e_2) = r(N)$.

With $\rho(N)$ the number of elements of $N$, the nullity is $n(N) = \rho(N) - r(N)$. An element $e$ is dependent on $N$ if $r(N+e) = r(N)$. A circuit of $r$ is a minimal dependent set: a subset $P$ with $n(P) > 0$ such that $n(N) = 0$ for every proper subset $N$ of $P$. In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.

Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if

(C₁) No proper subset of a circuit is a circuit.

(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.

In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.

Rank from circuits. Whitney defines (p. 516):

Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.

In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset $N$.

Formalization targets

Goal: the two systems are equivalent

For every finite set $M$:

$$\text{(1)}\quad r \text{ satisfies } (\mathrm R) \;\Longrightarrow\; \mathcal C(r) \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C(r),\ r_{\mathcal C(r)} = r;$$ $$\text{(2)}\quad \mathcal C \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C \;\Longrightarrow\; r_{\mathcal C} \text{ satisfies } (\mathrm R),\ \mathcal C(r_{\mathcal C}) = \mathcal C,$$

where $\mathcal C(r)$ is the family of circuits of $r$ and $r_{\mathcal C}$ is the rank defined from $\mathcal C$. This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."

Milestones, in the order the argument uses them

• Lemma 5 (p. 512): each element of a circuit is dependent on the rest of the circuit.
• Lemma 6 (p. 512): if $e \notin P_1$ is dependent on $P_1$ but on no proper subset of $P_1$, then $P_1 + e$ is a circuit.
• Theorem 4 (p. 512): for $e \notin N$, some circuit in $N + e$ contains $e$ if and only if $e$ is dependent on $N$.
• Theorem 5 (p. 513): if $N = e_1 + \cdots + e_p$ is formed element by element, $n(N)$ is the number of indices $i$ for which some circuit in $e_1 + \cdots + e_i$ contains $e_i$.
• §5 (pp. 512–513): the circuits of a rank system satisfy $(\mathrm C_1)$ and $(\mathrm C_2)$.
• Lemma 7 (p. 516): $r(e_1, \dots, e_{q-2}, e_{q-1}, e_q) = r(e_1, \dots, e_{q-2}, e_q, e_{q-1})$ under $(\mathrm C_1)$, $(\mathrm C_2)$.
• Lemma 8 (p. 517): the rank of a subset defined from circuits does not depend on the ordering of its elements.
• §8 (p. 517): the rank defined from circuits satisfies $(\mathrm R_1)$–$(\mathrm R_3)$.

Significance

The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.

On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of $\Gamma_i$, with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.

Difficulty

The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in $(\mathrm C_1)$, $(\mathrm C_2)$ obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where $(\mathrm C_2)$ does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, $(\mathrm C_2)$ for circuits of a rank function requires turning the local postulate $(\mathrm R_3)$ into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.

Formalization scope

• The elements form a finite type α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set $e_1, \dots, e_n$.
• Ranks and nullities are integers (ℤ), so that $n(N) = \rho(N) - r(N)$ is a true difference.
• Ordered sets of elements are lists. Lemmas 7, 8 and Theorem 5 assume the list has no repetitions, as Whitney's "ordered set of elements" means. "A circuit in $e_1 + \cdots + e_i$" means a circuit contained in $\{e_1, \dots, e_i\}$.
• The rank of a subset from circuits is computed along one fixed enumeration N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.
• Tacit hypothesis made explicit. Whitney's circuits are nonempty, since a circuit of a rank system has positive nullity. The family $\{\emptyset\}$ satisfies $(\mathrm C_1)$, $(\mathrm C_2)$ vacuously, but its circuit rank is $\rho$, which has no circuits, so the round trip fails. Part (2) of the goal therefore assumes $\emptyset \notin \mathcal C$, and part (1) asserts $\emptyset \notin \mathcal C(r)$.
• Lemma 6 assumes $e \notin P_1$, which the paper leaves tacit.
• Ruled out. Neither system may be encoded as Mathlib's Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.

The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under $(\mathrm R_1)$–$(\mathrm R_3)$ or invariance of rankSeq under prefix-preserving changes.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• Mathlib, Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

• 1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
• 1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
• 1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$, an order cost rate $c^d$, a shipment cost rate $c^r$, a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$, shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$, and $u^{(i)}$ denotes the sum of $i$ copies.

The state is $(\hat y, v^d, x^r)$:

• $\hat y = (y^1, \dots, y^L)$ lists the outstanding orders, $y^i$ placed $i$ periods ago;
• $v^d$ is the depot's echelon inventory (its own stock plus $x^r$);
• $x^r$ is the outlet's stock plus shipments in transit.

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$. With demand $u$, the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$. The one-period cost is

$$c^d(y) + h^d(v^d + y^L) + c^r z + R(x^r + z),$$

where $c^d(y) = K + c^d y$ for $y > 0$, $c^d(0) = 0$, and

$$R(x) = \alpha^l\{-h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r)E[x - u^{(l+1)}]^+\}.$$

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$.

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$. The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$, action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$. The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$: up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$. For every state with $\hat y \ge 0$ and $x^r \le v^d$, and every admissible policy $\pi$,

$$B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).$$

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$, $g_n^r$, $\hat g_n^d$, $g_n^d$ for the $n$-period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$, and of the depot with penalty $P$.

• Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$.
• Property (e): $g_n^r \to g^r = B^{r\alpha}$.
• §2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$.
• Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$.
• Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
• Lemma 3: $\hat g_n \to g^d + g^r$.
• Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$, built from the outlet's optimal costs $g_{n-1}^r$, and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$, and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$. Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$, and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

• Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$, whose index $k$ is the paper's $y^{k+1}$. For $L = 0$ the current order arrives at once.
• Policies and cost. Time runs forward with weight $\alpha^k$; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
• Finite-horizon programs. These are real infima over the feasible actions.
• Hypotheses. Statements quantify over the physical states $\hat y \ge 0$, $x^r \le v^d$. The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$, demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$; that is the paper's definition of $\pi_\alpha^*$, and its existence is Iglehart's.
• Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
• Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$, $n \ge 2$, and eventually, respectively. The moderation notes give the counterexample at $n = 1$. Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
• Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$, value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

• A. Federgruen, P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark, H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.

Timeline.

• Clark and Scarf (Management Science 1960) showed that the finite-horizon, discounted problem of a serial system decomposes: an optimal policy is obtained by solving the most downstream location alone, charging its shortfalls to the upstream location through an induced penalty cost, and then solving the upstream location as a single-location problem with that penalty.
• Iglehart (Management Science 1963, and a 1963 chapter in Multistage Inventory Models and Techniques) established the infinite-horizon theory of the single-location problem with a fixed order cost: optimality of stationary $(s,S)$ policies under discounted and average costs, and the convergence of value iteration.
• Federgruen and Zipkin (Operations Research 1984) carried the decomposition to the infinite horizon for a depot and one retail outlet, under discounted costs (Theorem 1) and under the average-cost criterion (Theorem 2). This mission is about the average-cost case, §3 of that paper.

Setting

Time is divided into periods. A depot orders from an outside supplier with lead time $L \ge 0$ and supplies a retail outlet with shipment lead time $l \ge 0$. The demand $u$ in each period is a nonnegative random variable with law $\nu$ and finite mean $\mu$; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.

The state is $(\tilde y, v^d, x^r)$:

• $\tilde y = (y^1,\dots,y^L)$ lists the orders placed $1,\dots,L$ periods ago;
• $v^d$ is the depot's echelon inventory, its own stock plus the outlet's inventory position;
• $x^r$ is the outlet's inventory position, its stock plus shipments in transit.

In each period the decision is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$, where $y^L$ is the order arriving now. The state then moves to $((y, y^1,\dots,y^{L-1}),\, v^d + y^L - u,\, x^r + z - u)$.

Costs are a fixed order cost $K$, proportional order and shipment rates $c^d$ and $c^r$, a holding rate $h^d$ on system inventory, an extra holding rate $h^r$ at the outlet and a backorder penalty rate $p^r$. After the paper's accounting transformation, the one-period cost is

$$c^d(y) + D(v^d + y^L) + c^r z + R(x^r + z),$$

with $c^d(y) = K + c^d y$ for $y > 0$ and $c^d(0) = 0$, $D(v) = h^d v$, and, at $\alpha = 1$,

$$R(x) = -h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r) E[x - u^{(l+1)}]^+ ,$$

where $u^{(l+1)}$ is the demand over $l + 1$ periods. The critical number $x^{r*}$ is a minimizer of $R$. The stationary induced penalty is $P(x) = R(x) - R(x^{r*})$ for $x < x^{r*}$ and $0$ otherwise.

For a policy $\pi$ and initial state $s$, $B_n(s \mid \pi)$ is the expected cost of the first $n$ periods and $B(s \mid \pi) = \limsup_n B_n(s \mid \pi)/n$ is the average cost. Problem IH asks for a policy minimizing $B(s\mid\cdot)$ from every state. The depot problem IH$^d$ has states $(\tilde y, v^d)$, orders $y \ge 0$ and one-period cost $c^d(y) + D(v^d + y^L) + P(v^d + y^L)$. Its minimal average cost is $a^d$. The outlet problem has states $x^r$, shipments $z \ge 0$ and one-period cost $c^r z + R(x^r + z)$. The policy $\pi^*$ orders by an optimal stationary policy of IH$^d$ and ships $z = \max(0, \min(x^{r*}, v^d + y^L) - x^r)$: up to the critical number if the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 2 (p. 828)

With $\alpha = 1$ and $c^d = c^r = 0$, the policy $\pi^*$ is measurable and feasible from every physical state, and for every such state $s$ and every measurable feasible policy $\pi$,

$$B(s \mid \pi^*) \le B(s \mid \pi).$$

Milestones

• Property (f) (p. 824): $g^r_n(x)/n \to B^r(x) = c^r\mu + R(x^{r*})$ for the outlet program $g^r_n$.
• Eq. (4) (p. 823), for $0 \le \alpha \le 1$: $\hat g_n(\tilde y, v^d, x^r) = \hat g^d_n(\tilde y, v^d) + g^r_n(x^r)$.
• §3 claims (p. 828): with $c^r = 0$, $x^{r*}$ is the critical number of every period, $g^r_n(x) = nR(x^{r*})$ for $x \le x^{r*}$, $\hat P_n = P$, $\hat g^d_n = g^d_n$ and $\hat g_n = g_n$.
• §3 display (p. 828): $\hat g_n(\tilde y, v^d, x^r)/n \to a = a^d + R(x^{r*})$.
• Lemma 5 (p. 828): $B(s \mid \pi^*) = a$.
• Proof of Theorem 2 (p. 828): $\hat g_n(s) \le B_n(s \mid \pi)$ for every measurable feasible $\pi$.

Significance

The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location $(s,S)$-type problem for the depot with a known convex penalty $P$, and a myopic critical-number rule for the outlet. The optimal system cost is the sum $a^d + a^r$ of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":

• the class of measurable history-dependent policies;
• the expected costs of policies with unbounded one-period costs;
• the passage from history-dependent to Markov policies;
• the transient of $\pi^*$ when the outlet starts above its critical number.

Difficulty

The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that $\pi^*$ attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions $K$-convex rather than convex.

The paper's route avoids that equation but needs three separate facts:

• value iteration for the whole system, divided by $n$, converges to $a^d + a^r$, which rests on Iglehart's convergence for the depot and on the stationarity of the penalties when $c^r = 0$;
• the finite-horizon value bounds the cost of every history-dependent policy, not only of Markov ones;
• $\pi^*$ achieves $a$ from every state, including states with $x^r > x^{r*}$, where it does not ship at all until demand has brought the outlet below its critical number.

Formalization scope

• Representation. A state is a triple in $(\mathrm{Fin}\,L \to \mathbb R) \times \mathbb R \times \mathbb R$. For $L = 0$ the order placed now arrives at once. Time runs forward in Lean; the paper numbers periods backward. Finite-horizon value functions keep the paper's index $n$ (periods remaining). Each "min" of programs (1), (2), (3), (5) is a real infimum over the constraint set.
• Policies and costs. Policies are deterministic, history-dependent and measurable, and they must be feasible along every demand realization. $B_n$ is an extended real (expected positive part minus expected negative part of each period's cost). $B$ is a $\limsup$ in the extended reals, and the optimal average costs are infima in the extended reals.
• Standing assumptions (p. 821):
  • $K, h^d, h^r, p^r > 0$;
  • demands i.i.d., nonnegative, without atoms ("for convenience we shall assume $u$ is continuous") and with finite mean.
• Added hypotheses.
  • States are restricted to the physical ones, $\tilde y \ge 0$ and $x^r \le v^d$.
  • $c^d = c^r = 0$. The paper reduces to this case "without loss of generality", on the grounds that average proportional costs equal $c^d\mu$ and $c^r\mu$ "under all interesting policies" (p. 827). That class is never specified, and the proofs are written for $c^d = c^r = 0$. The general-cost version is the paper's informal reduction and is not part of the goal.
  • Eq. (4) is stated for $0 \le \alpha \le 1$ with $K, h^d, h^r, p^r > 0$ and $c^d, c^r \ge 0$ (so that it covers §3's case $c^d = c^r = 0$), and with the relation $\alpha^l p^r \ge (1 - \alpha^l)h^d$, which the paper names on p. 827; it holds automatically at $\alpha = 1$.
• Ruling out trivial readings.
  • $\pi^*$ is built from a depot rule $\sigma^d$ assumed optimal for IH$^d$ from every depot state. Its existence is Iglehart's theorem, cited and not formalized; no $(s,S)$ form is required.
  • The goal quantifies over all measurable feasible policies, and $\pi^*$'s own feasibility is a conclusion, so a vacuous policy class cannot satisfy it.
  • A sorry-free check in the workspace exhibits an instance (exponential demand) meeting every standing hypothesis other than the optimality of $\sigma^d$, including the existence of $x^{r*}$.
• Reusable infrastructure. The definitions of history-dependent policies and of extended-real expected and average costs for controlled processes driven by i.i.d. real noise are generic, and could be reused for other inventory and queueing models. Contributions are welcome on any milestone, and especially on a formal version of the Markov reduction (Dynkin–Yushkevich III.1) for this setting and on Iglehart's convergence of $g^d_n/n$.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. L. Iglehart, Dynamic Programming and Stationary Analyses of Inventory Problems, Chapter 1 in H. Scarf, D. Gilford and M. Shelly (eds.), Multistage Inventory Models and Techniques, Stanford University Press, 1963.
• E. B. Dynkin and A. A. Yushkevich, Controlled Markov Processes, Springer, 1979.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

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