Operations Research

Bandit Algorithms Linear algebra Machine Learning·Captain: mikedeng1

Feature-Based Dynamic Pricing: The EllipsoidPricing Algorithm Has Worst-Case Regret O(R d² ln(T/d))Research Paper

Motivation

Online marketplaces, ad exchanges and real-estate platforms sell items that are each described by a vector of features and are rarely seen twice. A seller who prices such items cannot learn a demand curve item by item. It must learn how features map to values, while pricing, from accept/reject feedback alone. Cohen, Lobel and Paes Leme (Management Science, 2020; SSRN 2737045) model this as feature-based dynamic pricing with adversarial features and a linear valuation. They show that a direct multi-dimensional binary search (PolytopePricing) can have regret exponential in the dimension (their Theorem 1). Their EllipsoidPricing algorithm, a pricing variant of Khachiyan's ellipsoid method (Khachiyan 1979), has worst-case regret quadratic in the dimension and logarithmic in the horizon (their Theorem 2). This mission formalizes Theorem 2 and the chain of lemmas behind it.

Setting

Fix a dimension $d \ge 2$ , a radius $R > 0$ and a horizon $T$ . Nature picks an unknown parameter $\theta \in \mathbb{R}^d$ with Euclidean norm $\|\theta\| \le R$ . In each period $t = 1, \dots, T$ a product arrives with a feature vector $x_t \in \mathbb{R}^d$ , $\|x_t\| \le 1$ , and market value $\theta' x_t$ . The seller sees $x_t$ , posts a price $p_t$ , and a sale occurs iff $p_t \le \theta' x_t$ , earning $p_t$ . The regret (Eq. (1)) is

\mathrm{Regret} = \sum_{t=1}^{T} \big[\theta' x_t - p_t\,\mathbb{I}\{\theta' x_t \ge p_t\}\big],

and the worst-case regret of a policy is its maximum over $\theta$ and over nature's (possibly adaptive) choice of features.

An ellipsoid with center $a$ and positive definite shape matrix $A$ is $E(A,a) = \{\theta : (\theta - a)' A^{-1} (\theta - a) \le 1\}$ . EllipsoidPricing with parameter $\epsilon > 0$ keeps an ellipsoid $E_t = E(A_t, a_t)$ , starting from the ball $E_1 = B(0,R)$ . In period $t$ it computes

\underline b_t = x_t' a_t - \sqrt{x_t' A_t x_t}, \qquad \bar b_t = x_t' a_t + \sqrt{x_t' A_t x_t},

the minimum and maximum of $\hat\theta' x_t$ over $E_t$ .

If $\bar b_t - \underline b_t \le \epsilon$ , it exploits: it posts $p_t = \underline b_t$ and keeps $E_{t+1} = E_t$ .
Otherwise it explores: it posts $p_t = \tfrac12(\bar b_t + \underline b_t)$ and replaces $E_t$ by the ellipsoid of Eq. (4) that covers the half of $E_t$ consistent with the feedback. With $b = A_t x_t / \sqrt{x_t' A_t x_t}$ , the new shape is $\tilde A = \frac{d^2}{d^2-1}\big(A_t - \frac{2}{d+1} b b'\big)$ and the new center is $a_t \pm \frac{1}{d+1} b$ , with $+$ after a sale.

Write $\lambda_d(A)$ for the smallest eigenvalue of a symmetric matrix $A$ .

Formalization targets

Goal: Theorem 2

There is a universal constant $C > 0$ such that for all $d \ge 2$ , $R > 0$ , $T \ge 2d$ , $\|\theta\| \le R$ and $\|x_t\| \le 1$ , EllipsoidPricing run with $\epsilon = R d^2 / T$ satisfies

\mathrm{Regret} \le C \, R \, d^2 \ln(T/d).

This is the paper's $O(R d^2 \ln(T/d))$ claim, with no constant fixed.

Milestones, in the order of the paper's argument

the closed forms of $\underline b_t, \bar b_t$ (§5.2);
the containment of each half-ellipsoid in the updated ellipsoid (Eq. (4), already proved on the platform);
$\theta \in E_t$ and $A_t \succ 0$ along the run;
the volume formula $\operatorname{Vol} E(A,a) = V_d \sqrt{\prod_i \lambda_i(A)}$ and the volume decrease $\operatorname{Vol} E(\tilde A) \le e^{-1/2d} \operatorname{Vol} E(A)$ (§5.1);
Lemma 2: if $z < \lambda_d(A)$ and $\det(A - \beta b b' - zI) \ge 0$ , then $\lambda_d(A - \beta b b') \ge z$ ;
Lemma 3: $\lambda_d(\tilde A) \ge \frac{d^2}{(d+1)^2} \lambda_d(A)$ ;
Lemma 4: if $\lambda_d(A) \le \epsilon^2/(400 d^2)$ and $x' A x > \epsilon^2/4$ , then $\lambda_d(\tilde A) \ge \lambda_d(A)$ ;
the eigenvalue floor $\lambda_d(A_t) \ge \epsilon^2 / (400 (d+1)^2)$ ;
Lemma 1: at most $2 d^2 \ln(20 R (d+1)/\epsilon)$ exploration periods;
an exploitation period sells and has regret at most $\epsilon$ .

Significance

The result. Theorem 2 shows that contextual posted-price learning with adversarial features costs only polynomially many "probing" sales in the dimension. A direct cutting-plane search over the polytope of consistent parameters (PolytopePricing) cannot do this: its worst-case regret is exponential in $d$ (Theorem 1). The ellipsoid analysis via the smallest eigenvalue (Lemmas 2–4) is reused in the paper's noisy-valuation extension (ShallowPricing, §6) and in later work on contextual pricing and contextual search.

Formalizing it. No part of the paper is machine-checked. The Eq. (4) containment is already proved on the platform (Bertsimas–Tsitsiklis Theorem 8.1). The volume factor there is $e^{-1/(2(d+1))}$ , weaker than the $e^{-1/2d}$ used here. The eigenvalue lemmas on rank-one perturbations (Lemmas 2–4) are new to the platform and reusable for any analysis of ellipsoid-type updates. A formal proof of the goal would also settle a gap in the printed proof, noted under the formalization scope.

Difficulty

The obvious argument is the textbook ellipsoid bound: volume shrinks by $e^{-1/2d}$ per exploration, so exploration must stop. This fails because the ellipsoid need not become small in every direction. The volume can go to zero while one axis stays long, and then a feature along that axis keeps triggering exploration. The paper replaces the volume argument by a lower bound on the smallest eigenvalue, which needs a sign analysis of the characteristic polynomial of a rank-one perturbation (Lemmas 2–4) together with the exploration test $x_t' A_t x_t > \epsilon^2/4$ . The constant $k = 1/(400 d^2)$ in Lemma 4 is chosen to make a specific inequality hold for every $d \ge 2$ .

The regret bound needs, in addition, a per-round bound for exploration periods. The printed proof (p. 16) uses "the trivial bound of regret $R$ per round". That bound is not immediate when an exploration price is accepted, since the center $a_t$ can leave $B(0,R)$ and the round's regret is then only bounded by $\sqrt{x_t' A_t x_t}$ . This is why the goal is the $O$ -form with an unspecified universal constant rather than the proof's explicit inequality.

Formalization scope

Types. Vectors are Fin d → ℝ; $\theta' x$ is the dot product θ ⬝ᵥ x. Both norms are Euclidean, encoded as $x\cdot x \le 1$ and $\theta\cdot\theta \le R^2$ ; Mathlib's ‖·‖ on Fin d → ℝ is the sup norm and is never used. Ellipsoids, the ball, and the update (4) are the published LinearOptimization.ellipsoid, ellipsoidBall, ellipsoidUpdateCenter and ellipsoidUpdateMatrix.
Eigenvalues and volume. $\lambda_d(A)$ is the infimum of the real spectrum, i.e. the minimum eigenvalue of a symmetric matrix. Volumes are Lebesgue measure on Fin d → ℝ in $[0, \infty]$ . $\varphi_D(z)$ is $\det(D - zI)$ as printed, not Mathlib's charpoly.
The algorithm. EllipsoidPricing is a deterministic recursion indexed from $0$ (Lean period $t$ is the paper's $t+1$ ), started from $E_1 = B(0,R)$ , which the paper allows ("or in fact any ellipsoid that contains $K_1$ ", p. 11). The paper's "smallest ellipsoid containing $H_{t+1}$ " is replaced by its closed form (4), which the paper gives on p. 14. Because the algorithm is deterministic, a closed-loop nature generates a fixed feature sequence, and the worst case is a universal quantifier over $\theta$ in the ball and over sequences.
Added hypotheses, all disclosed in the items.
- $d \ge 2$ everywhere, since (4) divides by $d^2 - 1$ .
- $T \ge 2d$ in the goal, since $\ln(T/d) \le 0$ for $T \le d$ .
- $\epsilon \le 20 R (d+1)$ in Lemma 1 and the eigenvalue floor: for larger $\epsilon$ the printed bound is negative.
- $\|x\| \le 1$ in Lemma 4, the §3 normalization that its proof uses.
Not taken from the page. E₁ is not the Löwner–John ellipsoid of a general $K_1$ : the proof's " $\tilde E_1$ lies in the ball of radius $R$ " fails for it. The proof's explicit inequality $\mathrm{Regret} \le NR + (T-N)\epsilon$ is not a milestone, because of the per-round gap above.
Ruled out. The goal may not be trivialized by any of the following:
- a constant $C$ that depends on $d$ , $R$ , $T$ or the instance;
- regret measured against a price the algorithm never posts, or an exploit price that is not accepted;
- features bounded in the sup norm;
- an explore test or update different from (4);
- a single fixed feature sequence.
Contributions welcome. Proofs of the volume formula and the $e^{-1/2d}$ decrease, which are reusable for any ellipsoid-method development; the eigenvalue lemmas; and the per-round bound for accepted exploration prices that the goal needs.

Selected references

M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485 (authors' copy: https://ssrn.com/abstract=2737045)
L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20(1), 1980. https://doi.org/10.1016/0041-5553(80)90061-0
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
G. H. Golub, Some modified matrix eigenvalue problems, SIAM Review 15(2), 1973. https://doi.org/10.1137/1015032
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 8.1, the platform's ellipsoid update).

16 thms3 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

Contraction Mappings in the Theory Underlying Dynamic Programming 2: Under N-Stage Contraction and Monotonicity the Optimal Return Is the Unique Fixed Point of the Maximization OperatorResearch Paper

Motivation

Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return $f$ solves the optimality equation $v = Av$ , where $A$ maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return $h$ , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.

The plain contraction assumption (each one-step operator shrinks distances by a factor $c<1$ ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only $N$ steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.

Timeline:

1953: Shapley proves that the value of a discounted stochastic game is the fixed point of a contraction.
1960: Howard introduces policy iteration for finite discounted Markov decision processes.
1962–1965: Blackwell studies discrete and discounted dynamic programming, including the existence of optimal stationary policies.
1967: Denardo, in this paper, states the contraction and monotonicity assumptions for an abstract return and proves Theorems 1–4.
1977: Bertsekas, "Monotone mappings with application in dynamic programming", drops contraction and keeps only monotonicity.

Setting

Let $\Omega$ be a set of points. Each point $x$ has a decision set $D_x$ . A policy $\delta$ picks a decision $\delta_x\in D_x$ at every point, so the policy space is $\Delta=\times_{x\in\Omega}D_x$ . Let $V$ be the bounded real functions on $\Omega$ with the metric $\rho(u,v)=\sup_x|u(x)-v(x)|$ ; $V$ is complete. Write $u\ge v$ when $u(x)\ge v(x)$ for every $x$ .

The return $h$ assigns a real number $h(x,d_x,v)$ to each point $x$ , decision $d_x\in D_x$ and $v\in V$ . It defines two kinds of operators on $V$ :

[H_\delta v](x)=h(x,\delta_x,v),\qquad (Av)(x)=\sup_{d_x\in D_x}h(x,d_x,v),

and both are assumed to map $V$ into $V$ . An operator $B$ on $V$ has modulus $c$ or less when $\rho(Bu,Bv)\le c\,\rho(u,v)$ for all $u,v$ .

Monotonicity assumption: if $u\ge v$ then $H_\delta u\ge H_\delta v$ for every $\delta$ .
N-stage contraction assumption: for a positive integer $N$ and a number $c<1$ , both independent of $\delta$ , every $H_\delta^N$ has modulus $c$ or less and every $H_\delta$ has modulus $1$ or less.

Under these assumptions $H_\delta^N$ is a contraction, so it has a unique fixed point $v_\delta$ , the return function of $\delta$ . The optimal return is $f(x)=\sup_\delta v_\delta(x)$ . The auxiliary operator $E$ is $(Ev)(x)=\sup_\delta(H_\delta^Nv)(x)$ .

Formalization targets

Goal: Theorem 4 (p. 169)

Under the monotonicity and N-stage contraction assumptions:

\text{(a) } H_\delta v_\delta=v_\delta \text{ and } v_\delta \text{ is the only fixed point of } H_\delta;\qquad \text{(b) } \rho(v_\delta,v)\le\frac{\rho(H_\delta v,v)\,N}{1-c};

\text{(c) } E \text{ has modulus } c \text{ or less};\qquad \text{(d) } f\in V,\ Ef=f,\ Af=f,\ \text{ and } f \text{ is the only fixed point of } E \text{ and of } A;

\text{(e) } v\le f\ \Longrightarrow\ \rho(A^Nv,f)\le c\,\rho(v,f).

Milestones

The observation at the end of §3 (p. 168): if every operator in a nonempty family has modulus $c$ or less, then their pointwise supremum has modulus $c$ or less, provided it maps $V$ into $V$ .
Lemma 1 (p. 168): under monotonicity, $A$ is monotone; $Av\ge v$ implies that $A^nv$ is nondecreasing in $n$ ; $H_\delta v\ge v$ implies that $H_\delta^nv$ is nondecreasing in $n$ .
Theorem 4 (a)–(c), the part the paper proves in the text of §5 before stating the theorem. This milestone also includes the existence of $E$ as an operator on $V$ and $f\in V$ .
Lemma 2 (p. 169): $Av\le v$ implies $v\ge f$ , and $Av\ge v$ implies $v\le f$ ; $Av_\delta\ge v_\delta$ ; $H_\delta v\ge v$ implies $v_\delta\ge H_\delta v$ .

The mission also contains two consequences that are not milestones: $f$ is optimal for the mathematical programs $\min v$ s.t. $Av\le v$ and $\max v$ s.t. $Av\ge v$ (§6, p. 171), and a policy is optimal exactly when it attains $f(x)=h(x,\delta_x,f)$ at every point (§7, p. 173).

Significance

Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation $v=Av$ has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that $f$ is the least $v$ with $Av\le v$ and the greatest $v$ with $Av\ge v$ . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization $\Delta^*=\Delta^+$ reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.

The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after $N$ steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.

Difficulty

The obvious argument would apply the Banach fixed-point theorem to $A$ . That does not work: under the N-stage assumption, $A^N$ need not be a contraction. The paper gives an example (p. 170) with $N=2$ , $c=\tfrac12$ , where $A^n$ has modulus $1$ for every $n$ . The supremum over decisions does not commute with composition, so the contraction of each $H_\delta^N$ says nothing directly about $A^N$ . The paper therefore works through the auxiliary operator $E$ , which is a contraction. The hard step is to show that $f$ , the supremum of the policy returns, is a fixed point of $A$ . This is the second half of Lemma 2(a), an $\varepsilon$ -argument that uses both monotonicity and the modulus- $1$ bound on $H_\delta$ .

Part (e) holds only for $v\le f$ . It is not a contraction property of $A^N$ on all of $V$ .

Formalization scope

$V$ is lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is $\rho$ . The order is pointwise (PLe).
$H$ , $A$ and $E$ are given as functions $V\to V$ , which is the paper's "range contained in $V$ ". They are tied to $h$ by IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including $f$ (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.
"Modulus $c$ or less" is the inequality ModulusLE B c. NStageContractionAssumption H N c holds $0<N$ , $c<1$ , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with $N$ and $c$ independent of $\delta$ .
The return functions are a family v with $H_\delta^Nv_\delta=v_\delta$ , the paper's §5 definition. $H_\delta v_\delta=v_\delta$ is the conclusion (a), never a hypothesis.
In the goal, $E$ is an operator with IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. $f$ is never defined as a fixed point of $A$ or $E$ . The goal asserts that the pointwise least upper bound of $\{v_\delta(x)\}$ exists in $V$ and is the unique fixed point of both.
The trivializing formalizations are ruled out explicitly: assuming $H_\delta v_\delta=v_\delta$ , defining $f$ as $A$ 's fixed point, or dropping $v\le f$ from (e) would each change the theorem.

A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to $H_\delta^N$ ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.

Selected references

E. V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2) (1967) 165–177. https://doi.org/10.1137/1009030
L. S. Shapley, Stochastic Games, Proc. Nat. Acad. Sci. 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36 (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. P. Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031

7 thms3 active usersReviewed

Completed

Dynamical Systems Stochastic Systems·Captain: mikedeng1

Stability and Instability of Fluid Models for Reentrant Lines 1: Every Work-Conserving Fluid Model of the Three-Buffer Line 1→2→1 Is Stable When m₁ + m₃ < 1 and m₂ < 1Research Paper

Why reentrant lines, and why this one

A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.

Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.

Timeline:

1993: Kumar conjectured that the three-buffer line $1 \to 2 \to 1$ is stable under the first-in-first-out (FIFO) discipline whenever the load condition holds, for exponential distributions.
1993: Wang proved that the FIFO fluid model of this line is stable, which with Dai's theorem confirms the conjecture.
1996: Dai and Weiss (Theorem 3.1) proved stability of the fluid model for every work-conserving discipline, with an explicit emptying time.

Setting

A reentrant line has $I$ stations and $K$ classes. Fluid enters as class $1$ at rate one; class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and service rate $\mu_k = 1/m_k$ , and on completion becomes class $k+1$ (class $K$ leaves). The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$ , and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$ .

A fluid model solution is a pair of paths $Q(t) \in \mathbb R^K$ (fluid levels) and $T(t) \in \mathbb R^K$ (cumulative time spent serving each class) such that, for $t \ge 0$ :

Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t)\quad(\mu_0T_0(t) = t),\qquad Q_k(t) \ge 0,

each $T_k$ starts at $0$ and is nondecreasing, and the idle time $U_i(t) = t - B_i(t)$ , with busy time $B_i(t) = \sum_{k \in C_i} T_k(t)$ , is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$ .

A set of fluid model solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$ .

The three-buffer line of Figure 1 has $I = 2$ , $K = 3$ and route $1 \to 2 \to 1$ : classes $1$ and $3$ at station $1$ , class $2$ at station $2$ . The load condition (3.1) is

\rho_1 = m_1 + m_3 < 1, \qquad \rho_2 = m_2 < 1 .

Formalization targets

Goal: Theorem 3.1

m_1, m_2, m_3 > 0,\ \ m_1 + m_3 < 1,\ \ m_2 < 1 \ \Longrightarrow\ \text{the work-conserving fluid model (1.8)–(1.13) of } 1 \to 2 \to 1 \text{ is stable.}

The goal fixes no emptying time: it asserts only that some $\delta > 0$ works, which is Definition 1.3.

Milestones, in attack order

Lemma 2.2 (ii): a nonnegative absolutely continuous $g$ with $\dot g(t) \le -\varepsilon$ almost everywhere where $g(t) > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
Display (3.2) (already proved on the platform): at a regular point, the maximum of finitely many functions has the derivative of every component that attains it.
Lemma 3.2: for nonnegative linear functions $G_i$ of $Q$ with (a) $\dot G_i \le -\varepsilon_i$ while $W_i > 0$ and (b) $G_i \le \min_{j \ne i} G_j$ while $W_i = 0$ , the maximum $G$ is absolutely continuous and nonnegative, and $\dot G(t) \le -\min_i \varepsilon_i$ at regular points with $G(t) > 0$ .
Drift identity (proof of Theorem 3.1): with $\theta = m_1/(m_1+m_3)$ , $G_1 = \theta Q_1^+ + (1-\theta)Q_3^+$ and $G_2 = Q_2^+$ , where $Q_k^+ = \sum_{l \le k} Q_l$ , one has $G_i(t) = G_i(0) + t - B_i(t)/\rho_i$ .
Drift rate: $\dot G_i(t) = -(1/\rho_i - 1) < 0$ whenever $W_i(t) > 0$ .
Condition (b): $W_1(t) = 0 \Rightarrow G_1(t) \le G_2(t)$ and $W_2(t) = 0 \Rightarrow G_2(t) \le G_1(t)$ .
Emptying time: every work-conserving solution with $|Q(0)| = 1$ is empty from $\max\{\rho_1/(1-\rho_1), \rho_2/(1-\rho_2)\}$ on.

Significance

Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.

The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.

Difficulty

The obvious approach is to split cases on the relative loads, as the paper notes ( $m_1 + m_3/m_2 < 1$ or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.

Formalization scope

All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:

Classes and stations are 0-based (Fin 3, Fin 2). The paper's class $k$ is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.
Paths are total functions ℝ → Fin K → ℝ; every equation is imposed only for $t \ge 0$ , and derivatives are taken at $t > 0$ (HasDerivAt).
Work conservation (1.13) is in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. This is equivalent to the paper's integral condition for continuous paths.
No Lipschitz continuity is assumed; it follows from (1.10)–(1.12).
$m_k > 0$ is an explicit hypothesis (the paper takes it for granted). $|Q(0)| = \sum_k Q_k(0)$ .
Lemma 2.2 (ii) is stated with $\dot g(t) \le -\varepsilon$ ; the paper prints $<$ , but every application uses $\le$ , and the stated version is the stronger lemma.
Lemma 3.2 is stated for any reentrant line with $I \ge 1$ stations, assuming only (1.8)–(1.12), as in the paper.

A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every $m$ satisfying (3.1), with $|Q(0)| = 1$ (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.

Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.

Selected references

J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115
J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
P. R. Kumar, Re-entrant lines, Queueing Systems 13, 87–110, 1993. https://doi.org/10.1007/BF01158927
A. N. Rybko and A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28, 199–220, 1992.
D. D. Botvich and A. A. Zamyatin, Ergodicity of conservative communication networks, Rapport de recherche 1772, INRIA, 1992.

10 thms3 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case 2: General Demand: Sym-k-Concave Profit-to-Go, Optimal (s, S, A, p) PolicyResearch Paper

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$ -concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$ . At the start of period $t$ , the firm has inventory $x$ , which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$ . If $y>x$ , it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$ . After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$ . The corresponding price is $P_t(d)$ , the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$ .

Actual demand is $\alpha_t d+\beta_t$ . The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$ , with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$ . No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$ , incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$ . For a post-order inventory $y$ and expected demand $d$ , write

g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$ . This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$ -convex real function $f$ satisfies

f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$ . A function is symmetrically $k$ -concave when its negative is symmetrically $k$ -convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$ , then for every period

G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$ . An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$ , and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$ .

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$ -convexity to symmetric $k$ -convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$ -convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$ , that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$ -concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$ . The statement must assert Bellman optimality at every $x$ , including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$ , matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$ , with $T>0$ and terminal value $v_{T+1}=0$ . Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$ . The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$ .

The formal assumptions include $k\ge0$ and $c_t\ge0$ , and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$ .

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

12 thms3 active usersReviewed

Discrete Geometry Linear Optimization Probability·Captain: mikedeng1

A Friendly Smoothed Analysis of the Simplex Method: Gaussian-Perturbed Shadows Have at Most 3 + 128πe²d²√(log n)σ⁻²(1 + 4σ√(d log n))(1 + 16σ√(log n)) Expected EdgesResearch Paper

Why the simplex method needs smoothed analysis

The simplex method solves linear programs quickly in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972). Smoothed analysis, introduced by Spielman and Teng (JACM 2004), explains the gap: it measures the expected running time when every constraint row of a worst-case input is perturbed by a small random amount of size $\sigma$ . For the shadow vertex pivot rule, the running time is controlled by a purely geometric quantity, the number of edges of a random polygon, and the smoothed complexity of the method is essentially an upper bound on that number.

Timeline (bounds on the expected shadow size of smoothed unit LPs, as surveyed in §1.1 of the paper). Borgwardt (1987) proved $\Theta(d^{1.5}\sqrt{\log n})$ for rows drawn from a centered Gaussian, asymptotically as $n\to\infty$ ; this is the case $\bar a_i=0$ of the model below. Spielman and Teng (2004) gave the first smoothed bound, $O(d^3n\sigma^{-6}+d^6n\log^3 n)$ . Deshpande and Spielman (FOCS 2005) improved the dependence on $\sigma$ to $O(dn^2\log n\,\sigma^{-2}+d^2n^2\log^2 n)$ . Vershynin (SIAM J. Comput. 2009) reduced the dependence on $n$ to polylogarithmic, $O(d^3\sigma^{-4}+d^5\log^2 n)$ . Dadush and Huiberts (arXiv:1711.05667, STOC 2018, SIAM J. Comput. 2020) proved $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^{2.5}\log n\,\sigma^{-1}+d^{2.5}\log^{1.5}n)$ for Gaussian perturbations by a simpler argument, which also gives bounds for Laplace perturbations.

Setting

Fix dimensions $n\ge d\ge3$ and a shadow plane, a two-dimensional linear subspace $W\subseteq\mathbb R^d$ , chosen independently of the randomness. The constraint vectors $a_1,\dots,a_n\in\mathbb R^d$ are independent, and $a_i\sim N_d(\bar a_i,\sigma)$ is Gaussian with center $\bar a_i$ , $\|\bar a_i\|\le1$ , and standard deviation $\sigma>0$ in every coordinate, i.e. with density $(2\pi\sigma^2)^{-d/2}e^{-\|x-\bar a_i\|^2/(2\sigma^2)}$ .

Let $Q=\operatorname{conv}(a_1,\dots,a_n)$ . The shadow polygon is $Q\cap W$ . An edge of a convex set $K$ is a segment $[u,v]$ , $u\ne v$ , which is an extreme subset of $K$ ; $|\operatorname{edges}(K)|$ is the number of edges. The number of pivots of the shadow vertex method on the unit LP $\{x:Ax\le\mathbf1\}$ between two objectives spanning $W$ is at most $|\operatorname{edges}(Q\cap W)|$ (the paper's Lemma 11 and Theorem 12).

The proof passes through general row distributions with density $\mu$ and mean $y$ , described by four parameters: the log-Lipschitz constant $L$ ( $\mu(x)\le e^{L\|x-x'\|}\mu(x')$ ); the line variance $\tau^2$ (the least variance of $\mu$ restricted to a line); the $n$ -th deviation $r_n$ (the least $r$ with $\int_r^\infty\Pr[|(X-y)^\mathsf T\theta|\ge t]\,dt\le r/n$ for all unit $\theta$ ); and the cutoff radius $R_{n,d}$ (the least $R$ with $\Pr[\|X-y\|\ge R]\le 1/(d\binom nd)$ ). The Gaussian is not log-Lipschitz; the Laplace–Gaussian distribution $LG_d(\bar a,\sigma,r)$ , whose density equals the Gaussian one inside the ball of radius $r\sigma$ around $\bar a$ and decays like $e^{-\|x-\bar a\|r/\sigma}$ outside, replaces it.

Formalization targets

Goal: Theorem 13 with explicit constants

\mathbb E\big[|\operatorname{edges}(\operatorname{conv}(a_1,\dots,a_n)\cap W)|\big]\le 3+\frac{128\pi e^2 d^2\sqrt{\log n}}{\sigma^2}\big(1+4\sigma\sqrt{d\log n}\big)\big(1+16\sigma\sqrt{\log n}\big).

The paper states $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^{2.5}\log n\,\sigma^{-1}+d^{2.5}\log^{1.5}n)$ ; the constant above is the one its proof produces (Theorem 22's proof, Lemma 45, Lemma 46).

Intermediate targets (milestones)

the parametrized shadow bound (Theorem 22), $\mathbb E|\operatorname{edges}|\le 2+8\pi e^2d^{1.5}(L/\tau)(1+R_{n,d})(1+4r_n)$ ;
its ingredients: the edge-counting reduction (Lemma 25), the perimeter bound $2\pi(1+4r_n)$ (Lemmas 19, 26), the conditioning on bounded diameter (Lemma 29), the chord combination calculus (Lemmas 35, 36), and the two expected-length bounds (Lemmas 39, 40, 41), together with the trade-off $LR(1/2)\ge d/3$ (Lemma 21);
the Gaussian specialisation: Laplace–Gaussian tails (Lemma 44), its parameters (Lemma 45), and the comparison with the Gaussian (Lemma 46).

Significance

The bound gives the best known smoothed complexity of a simplex method, with only $\sqrt{\log n}$ dependence on the number of constraints. Section 4 of the paper turns it into a complete two-phase shadow vertex algorithm with $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^3\log^{1.5}n)$ expected pivots. The parametrized Theorem 22 applies to any perturbation family with bounded parameters, so it also yields shadow bounds for Laplace and other noise models.

The result is proved; it has not been machine-checked. A formalization adds a verified chain from four distributional parameters to a polygon edge count. The intermediate statements have independent value: an expected-perimeter bound for random polygons, the deterministic chord-length identity for simplices, and tail estimates for the Laplace–Gaussian distribution.

Difficulty

The expected number of edges is a sum, over all $\binom nd$ index sets, of the probability that their simplex meets $W$ in an edge; there are far too many terms for per-set estimates to give a bound polylogarithmic in $n$ . The paper's route (inspired by Kelner and Spielman) instead compares the expected perimeter with the expected length of an edge, and the hard part is a lower bound on the expected length of an edge conditioned on it appearing. That conditioning is on a probability-zero configuration (the simplex lying in a fixed hyperplane), and its analysis needs Blaschke's change of variables, the shape decomposition of the simplex, and log-Lipschitz shifts of densities. On the Gaussian side, the density is not log-Lipschitz, which forces the Laplace–Gaussian detour and a comparison of edge counts under two different laws.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d), $[n]$ is Fin n, $\log$ is the natural logarithm. The Gaussian is the published SmoothedSimplex.Shadow.gaussian, the edge relation is the published Hirsch.Adj, and the rows' joint law is Measure.pi. Edges are segments counted once; the perimeter is the sum of edge lengths. Expectations are lower Lebesgue integrals in $[0,\infty]$ , and every edge-count bound also asserts almost-everywhere measurability of the count, so the integral is a genuine expectation. Conditional expectations are stated multiplied out (no division by a probability), and the parameters of Definitions 15–18 are upper-bound predicates (lower bound for the line variance), which is how every statement of the paper uses them.

Hypotheses added relative to the page, each implicit there: $\sigma>0$ ; $L,\tau>0$ and $R,r\ge0$ in Theorem 22; positivity of log-Lipschitz densities; the standing $n\ge d\ge3$ of §3 in Lemma 44. Lemmas 39 and 41 are stated on the explicit conditional densities that the paper derives in Lemma 37, instead of through regular conditional distributions; Lemma 39 takes the conclusion $d/3\le LR$ of Lemma 21 as a hypothesis, as its proof uses it. Two printed slips are corrected: Lemma 46's formula is stated for $\operatorname{conv}(a_1,\dots,a_n)\cap W$ , as its sentence and proof have it, and Lemma 35 refers to Definition 33 (not 34).

The goal mentions only Gaussian rows, $W$ , and the edge count of $\operatorname{conv}(a)\cap W$ . It cannot be trivialized by an unsatisfiable parameter hypothesis or a bound on edge lengths, since it has neither; and it counts edges of the polygon, not of the polytope $\operatorname{conv}(a)$ .

A complete development needs: Gaussian and Laplace–Gaussian tail bounds; measurability of the edge count of a random polygon; the perimeter monotonicity of convex sets; Blaschke's change of variables (Theorem 7 of the paper, quoted from Blaschke 1935), which Mathlib does not have; and the regular conditioning of Lemmas 32, 37 and 38. The Blaschke formula, the perimeter facts for convex polygons, and the tail bounds are reusable well beyond this mission. Contributions to any milestone, or to these supporting results as separate theorems, are welcome.

Selected references

D. Dadush, S. Huiberts, A Friendly Smoothed Analysis of the Simplex Method, SIAM J. Comput. 49(5), 2020 (STOC 2018); preprint arXiv:1711.05667v4, 2019. https://arxiv.org/abs/1711.05667
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3), 2004. https://doi.org/10.1145/990308.990310
R. Vershynin, Beyond Hirsch Conjecture: Walks on Random Polytopes and Smoothed Complexity of the Simplex Method, SIAM J. Comput. 39(2), 2009. https://doi.org/10.1137/070683386
A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005 (cited as [DS05] in the paper).
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972 (cited as [KM70] in the paper).

20 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter $\delta$ : a solution must satisfy $x\in\mathcal X_\delta$ for every $\delta$ in a possibly infinite set $\Delta$ . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws $N$ independent samples of $\delta$ , solves the convex program with those $N$ constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.

Timeline.

Calafiore and Campi (Math. Program. 2005; IEEE TAC 2006) introduced the method and bounded the probability that the violation exceeds $\varepsilon$ by a quantity of order $\binom Nd(1-\varepsilon)^{N-d}$ . The bound is valid but loose.
Campi and Garatti (SIAM J. Optim. 2008, this mission's source) proved the bound $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for every convex problem satisfying existence and uniqueness of solutions. They showed it is attained with equality by every fully-supported problem, so it cannot be improved without further assumptions.
Later work extended the result to non-unique solutions, constraint removal, and non-convex decisions (Campi and Garatti, Introduction to the Scenario Approach, SIAM 2018).

Setting

Let $(\Delta,\mathcal D,\mathbb P)$ be a probability space, $c\in\mathbb R^d$ with $d\ge1$ , and let $\mathcal X\subseteq\mathbb R^d$ and $\mathcal X_\delta\subseteq\mathbb R^d$ ( $\delta\in\Delta$ ) be convex closed sets. The violation probability of a point $x$ is

V(x)=\mathbb P\{\delta\in\Delta:\ x\notin\mathcal X_\delta\}.

For a multi-extraction $(\delta^{(1)},\dots,\delta^{(m)})\in\Delta^m$ , the program $P_m$ minimises $c^\top x$ over $x\in\mathcal X\cap\bigcap_{i=1}^m\mathcal X_{\delta^{(i)}}$ . It is assumed that every $P_m$ has a unique solution $x^*_m$ . A constraint $\delta^{(r)}$ is a support constraint of $P_m$ if its removal changes the solution. A convex $P_m$ has at most $d$ support constraints (Proposition 2.2). The problem is fully-supported if, for every $m\ge d$ , the program $P_m$ built from $m$ independent samples has exactly $d$ support constraints with $\mathbb P^m$ -probability one.

Two further objects carry the argument. For $\mathcal I\subseteq\{1,\dots,m\}$ of cardinality $d$ , $S_{\mathcal I}$ is the set of multi-extractions whose support constraints have exactly the indexes in $\mathcal I$ . The violation law is

F(\alpha)=\mathbb P^d\{V(x^*_d)\le\alpha\},

the distribution of the violation of the solution built from $d$ samples.

Formalization targets

Goal: Theorem 2.4, equation (2.3)

For a fully-supported problem, every $N\ge d$ and every $\varepsilon\in[0,1]$ ,

\mathbb P^N\{V(x^*_N)>\varepsilon\}=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.

Milestones (PART 1 of §3)

Proposition 2.2: at most $d$ support constraints.
$S_{\bar{\mathcal I}}\subseteq\widetilde S_{\bar{\mathcal I}}$ for $\bar{\mathcal I}=\{1,\dots,d\}$ , where $\widetilde S_{\bar{\mathcal I}}$ is the set where $\delta^{(d+1)},\dots,\delta^{(m)}$ are not violated by the solution generated by $\delta^{(1)},\dots,\delta^{(d)}$ ; and $\widetilde S_{\bar{\mathcal I}}\subseteq S_{\bar{\mathcal I}}$ up to a probability-zero set.
(3.3): $\mathbb P^m\{S_{\mathcal I}\}=\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)$ for every $\mathcal I$ of cardinality $d$ .
(3.4): $\binom md\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)=1$ for all $m\ge d$ .
Moment uniqueness: $F(\alpha)=\alpha^d$ is the only distribution on $[0,1]$ satisfying (3.4).
(3.2): $F(\alpha)=\alpha^d$ .
Partition chain: $\mathbb P^N\{V(x^*_N)>\varepsilon\}=\binom Nd\int_{(\varepsilon,1]}(1-\alpha)^{N-d}F(\mathrm d\alpha)$ .
Integration by parts: $\binom Nd\int_\varepsilon^1(1-\alpha)^{N-d}\,d\,\alpha^{d-1}\,\mathrm d\alpha=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ .

Significance

The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on $N$ , $d$ and $\varepsilon$ can be smaller, because a fully-supported problem attains it. The distribution of $V(x^*_N)$ is then a Beta law, $\mathbb P^N\{V(x^*_N)\le\varepsilon\}$ being the probability that a $\mathrm{Binomial}(N,\varepsilon)$ variable is at least $d$ , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: $N$ is chosen so that the binomial tail is below a confidence level $\beta$ . Fact (3.2), that $V(x^*_d)$ has distribution function $\alpha^d$ whatever the problem, is a distribution-free statement of independent interest.

Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on $[0,1]$ given the moments $\int(1-\alpha)^k\,\mathrm dF=1/\binom{d+k}d$ , and the incomplete-beta identity for binomial tails.

Difficulty

The obvious route would compute the law of $V(x^*_N)$ directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of $V(x^*_d)$ only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than $d$ support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first $d$ constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by $d$ .

Formalization scope

Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.

Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so $\bar{\mathcal I}$ is $\{i : i<d\}$ and " $\delta^{(d+1)},\dots,\delta^{(m)}$ " are the indexes $j\ge d$ . $\mathbb P^m$ is Measure.pi (fun _ : Fin m => P). $V$ , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.

Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve $P_k$ and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of $\{(x,\delta):x\in\mathcal X_\delta\}$ and measurability of the solution maps, the same two hypotheses as the goal. No set $S_{\mathcal I}$ is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.

Conventions. $F$ is the push-forward measure violationLaw on $\mathbb R$ , with $F(\alpha)$ = violationLaw … (Set.Iic α). Integrals against $F$ are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over $[0,1]$ for $\int_0^1$ , and over $(\varepsilon,1]$ for $\int_\varepsilon^1$ in the partition chain, since that integral comes from the event $V>\varepsilon$ . The integration-by-parts identity is a real interval integral. Ranges are $1\le d$ , $d\le m$ , $d\le N$ and $0\le\varepsilon\le1$ .

Ruled out. A pointwise "exactly $d$ support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event $\{V(x^*_N)>\varepsilon\}$ or of $S_{\mathcal I}$ , or the identity $\mathbb P^m\{S_{\mathcal I}\}=\mathbb P^m\{\widetilde S_{\mathcal I}\}$ , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.

Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on $[0,1]$ , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.

Selected references

M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19(3) (2008) 1211–1230. https://doi.org/10.1137/07069821X
G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Math. Program. 102 (2005) 25–46. https://doi.org/10.1007/s10107-003-0499-y
G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Trans. Automat. Control 51(5) (2006) 742–753. https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, Introduction to the Scenario Approach, SIAM, 2018. https://doi.org/10.1137/1.9781611975444
A. N. Shiryaev, Probability, 2nd ed., Springer, 1996, Chapter II, §12. https://doi.org/10.1007/978-1-4757-2539-1

14 thms3 active usersReviewed

Completed

Optimal Transport Optimization Probability·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 1: Strong Duality — the Worst-Case Expectation over an Optimal-Transport Ball on a Polish Space Equals Its Dual over (λ, φ)Research Paper

Motivation

A probability model $\mu$ for a random element $X$ is rarely known exactly. Distributionally robust performance analysis replaces the single expectation $E_\mu[f(X)]$ by its worst case over all models within a prescribed distance of $\mu$ . When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of $\mu$ . That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.

Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.

Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on $\mathbb R^d$ . Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as $C[0,T]$ and $D[0,T]$ .

Setting

Let $S$ be a Polish space with Borel σ-algebra $\mathcal B(S)$ , and let $\mu$ be a probability measure on $S$ (the baseline model).

Cost (A1). $c : S\times S\to[0,\infty)$ is lower semicontinuous, and $c(x,y)=0$ if and only if $x=y$ .
Performance function (A2). $f : S\to\mathbb R$ is upper semicontinuous and $\mu$ -integrable.
Budget. $\delta>0$ .

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ whose first marginal is $\mu$ and whose transport cost satisfies $\int c\,d\pi\le\delta$ . The second marginal of $\pi$ is the alternative model. The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ , and the primal value is

I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}.

The universal σ-algebra $\mathcal U(S)$ is the intersection of the completions of $\mathcal B(S)$ under all probability measures. Write $m\mathcal U(S;\bar{\mathbb R})$ for the $\mathcal U(S)$ -measurable functions $S\to[-\infty,\infty]$ . The dual feasible set $\Lambda_{c,f}$ consists of the pairs $(\lambda,\varphi)$ with $\lambda\ge0$ , $\varphi\in m\mathcal U(S;\bar{\mathbb R})$ and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$ . The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ , and the dual value is $J=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\}$ . Finally,

\varphi_\lambda(x)=\sup_{y\in S}\{f(y)-\lambda c(x,y)\}\in\mathbb R\cup\{\infty\}.

Formalization targets

Goal: Theorem 1

Under (A1) and (A2):

strong duality,

\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\};

there is $\lambda^*\ge0$ such that $(\lambda^*,\varphi_{\lambda^*})$ is a dual optimizer;
a feasible $\pi^*$ and a feasible $(\lambda^*,\varphi_{\lambda^*})$ with finite $J(\lambda^*,\varphi_{\lambda^*})$ are optimal with $I(\pi^*)=J(\lambda^*,\varphi_{\lambda^*})$ if and only if the complementary slackness conditions hold:

f(y)-\lambda^*c(x,y)=\varphi_{\lambda^*}(x)\ \ \pi^*\text{-a.s.},\qquad \lambda^*\Big(\int c\,d\pi^*-\delta\Big)=0.

The "if" direction is stated without the finiteness assumption.

Milestones

Weak duality $I\le J$ (5). Lemma 15. Strong duality with a primal optimizer on compact $S$ , first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of $\varphi_\lambda$ (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):

I=\inf_{\lambda\ge0}\Big\{\lambda\delta+E_\mu\Big[\sup_{y\in S}\{f(y)-\lambda c(X,y)\}\Big]\Big\}.

Significance

The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline $\mu$ . A modeller can therefore evaluate it by sampling from $\mu$ . Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from $x$ to maximizers of $f(z)-\lambda^*c(x,z)$ , and the budget is exhausted whenever $\lambda^*>0$ .

Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on $\mathbb R^m$ ). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.

Difficulty

The obvious route copies Kantorovich duality. That route fails here because the feasible set $\Phi_{\mu,\delta}$ fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces $S_n\times S_n$ . The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.

A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, $\varphi_\lambda$ need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction $y\in S_\pi$ from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces $C[0,T]$ and $D[0,T]$ .

Formalization scope

Space and costs. S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.
Extended reals. $I$ , $J$ , $I(\pi)$ , $J(\lambda,\varphi)$ and $\varphi_\lambda$ live in EReal. The integral of an extended-real function is $\int\varphi^+-\int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$ . A coupling with $\int f^-\,d\pi=\infty$ therefore never raises $I$ , which is the paper's reading in footnote 2.
Measurability and integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such $\varphi$ the lower integral equals the integral against the completion of $\mu$ .
Variants. The dual feasible set takes a set $K$ : with $K=S$ it is (6b), and with $K=S_\pi$ it is (29).
Hidden hypothesis. The "only if" part of Theorem 1(b) carries the hypothesis $J(\lambda^*,\varphi_{\lambda^*})<\infty$ . Without it the equivalence fails when $I=J=\infty$ .
Ruled-out trivializations. A primal that fixes both marginals (or neither), a dual over Borel-measurable $\varphi$ , and a Bochner integral for $\int f\,d\pi$ (which is $0$ off $L^1(\pi)$ ) all describe different problems and are ruled out by the definitions.
Infrastructure and contributions. Needed: Fenchel duality on $C_b(S\times S)$ and its dual $M(S\times S)$ (Riesz–Markov–Kakutani), Prokhorov's theorem, Sion's minimax theorem, and Jankov–von Neumann selection. Several are on the platform or in Mathlib, and all are reusable beyond this mission. Proofs of the milestones in any order, and of the posed Bertsekas–Shreve tools, are welcome.

Selected references

J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
D. Bertsekas and S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 7. MIT open copy
C. Villani, Optimal Transport: Old and New, Springer, 2008. doi:10.1007/978-3-540-71050-9

19 thms3 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Airline Seat Allocation with Multiple Nested Fare Classes 2: With Integer-Valued Demands an Optimal Integer Protection-Level Policy ExistsResearch Paper

Motivation

Airlines sell the seats of one flight leg at several prices. Cheaper fare classes tend to book earlier, so the seller must decide, as low-fare requests arrive, how many seats to hold back for later and more valuable passengers. The standard control is nested protection levels: a number $p_k$ of seats is reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain. Littlewood (1972) gave the optimal rule for two classes; Belobaba's EMSR heuristic (1987, 1989) extended it to many classes without an optimality guarantee.

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes (Operations Research 41(1), 1993) treat any number of classes with independent random demands and characterize optimal protection levels by first-order conditions on the expected revenue: Theorem 1 states that a policy with $f_{k+1}$ in the subdifferential of the expected revenue of the $k$ highest classes at $p_k$ , for every $k$ , is optimal. Their Theorem 2 addresses the question practitioners face first: seats and bookings are whole numbers. If demand is integer valued, is an optimal policy available among integer protection levels? The theorem answers yes. This mission formalizes that theorem and the chain of results in its proof.

Timeline.

Littlewood (1972): two fare classes, rule $f_2 = f_1 \Pr[X_1 > p_1]$ .
Belobaba (1987, 1989): EMSR heuristic for many classes.
Curry (1990) and Wollmer (1992): multiple nested classes, continuous and discrete demand respectively.
Brumelle and McGill (1993): subdifferential optimality conditions for any number of classes (Theorem 1), existence of an optimal integer policy for integer demand (Theorem 2), and the probability conditions (31) (Theorem 3).

Setting

Classes are numbered $k = 1, 2, \dots$ , class $1$ paying the highest fare. Class $k$ has a random demand $X_k \ge 0$ and fare $f_k$ , with $f_1 > f_2 > \cdots$ . The demands are mutually independent on a probability space $(\Omega, \mathcal F, P)$ . A protection-level policy is a sequence $p = (p_1, p_2, \dots)$ with $p_k \ge 0$ ; the dummy level $p_0 = 0$ is never used.

For a demand vector $x$ and $s$ available seats, the revenue of the $k$ highest classes is defined recursively (Eqs. (8)–(9), p. 130):

R_1[s; p; x] = \begin{cases} f_1 s & 0 \le s < x_1,\\ f_1 x_1 & x_1 \le s,\end{cases}

R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k,\\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1},\\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s.\end{cases}

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$ . A policy is optimal if it maximizes $ER_k[s; \cdot\,; X]$ for every $k$ and every $s \ge 0$ (p. 130).

For a function $g$ and $t \ge 0$ , $\delta_+ g(t)$ and $\delta_- g(t)$ are the right and left derivatives, with $\delta_- g(0) = +\infty$ , and the subdifferential is $\delta g(t) = [\delta_+ g(t), \delta_- g(t)]$ (p. 131). Condition (20) is

f_{k+1} \in \delta ER_k[p_k; (p_0, \dots, p_{k-1}); X], \qquad k = 1, 2, \dots

A function is CLBI (Concave and Linear Between Integers, p. 132) if it is concave on $s \ge 0$ and linear on each interval $[m, m+1]$ , $m = 0, 1, 2, \dots$

Formalization targets

Goal: Theorem 2 (p. 132)

If every $X_k$ is integer valued and the fares are positive, there is a policy $p^*$ with $p^*_k \in \{0, 1, 2, \dots\}$ such that

ER_k[s; q; X] \le ER_k[s; p^*; X] \qquad \text{for every policy } q,\ k \ge 1,\ s \ge 0,

and $p^*$ satisfies (20). The competitor $q$ ranges over all real protection levels.

Milestones (in proof order)

(27): $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$ , and $ER_1$ is CLBI.
Covering property (p. 132): if $g$ is CLBI and $\delta_+ g(s_2) < c < \delta_- g(s_1)$ with $s_1 < s_2$ , then $c \in \delta g(n)$ for an integer $n \in [s_1, s_2]$ .
(28)–(29): for $s \ge p_k$ ,

\delta_+ ER_{k+1}[s] = f_{k+1}\Pr[X_{k+1} > s - p_k] + \sum_{i=0}^{\lfloor s - p_k\rfloor} \delta_+ ER_k[s - i]\Pr[X_{k+1} = i],

and the analogous formula for $\delta_-$ at $s > p_k$ . 4. Corollary 1 (p. 131): concavity of $ER_k$ and $f_{k+1} \in \delta ER_k[p_k]$ give concavity of $ER_{k+1}$ . 5. CLBI propagation (p. 133): if $ER_k[\cdot; p^*; X]$ is CLBI and integer $p^*_1, \dots, p^*_k$ satisfy (20), then $ER_{k+1}[\cdot; p^*; X]$ is CLBI. 6. (30): for $s$ large enough, $\delta_+ ER_{k+1}[s; p; X] < f_{k+2}$ . 7. Theorem 1 (p. 131): a policy satisfying (20) is optimal.

Significance

The result. Theorem 2 justifies computing protection levels in whole seats: with integer demand, restricting to integer policies loses nothing against arbitrary real protection levels. The construction also shows that (20) is solvable at every level, so the sufficient condition of Theorem 1 is never empty for integer demand. Many later revenue-management models assume an optimal nested policy exists and rely on this result or its dynamic-programming analogues.

Formalizing it. The theorem is proved on the page by an induction on the class index, but several steps are compressed: (28)–(29) are printed without the range of $s$ on which they hold, and (30) is asserted "by recursive application". To our knowledge none of these statements has a machine-checked proof. A formal development gives a verified account of one-sided derivatives of expectations of piecewise-linear random functions and of the integer covering property. These pieces are reusable for other newsvendor-type and nested-inventory models. The probability-condition characterization (Theorem 3) is the subject of a companion mission in the same series.

Difficulty

Concavity of the expected revenue does not hold for arbitrary policies. It is only guaranteed level by level, when the protection level already chosen at level $k$ satisfies (20). Existence of an integer optimum therefore cannot be obtained by rounding a real optimum: the integer levels must be chosen one at a time, and each choice must preserve both concavity and the CLBI shape needed for the next. A second obstacle is analytic. The one-sided derivatives of $ER_{k+1}$ are expectations of derivatives of a random piecewise-linear function. Exchanging differentiation and expectation, and computing the sums in (28)–(29) exactly at integer and non-integer $s$ , is where informal arguments and formal ones diverge. Finally there are infinitely many classes, so the policy $p^*$ is an infinite sequence built by recursion.

Formalization scope

Model. Classes are indexed by $\mathbb N$ from $1$ ; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$ . Seats, demands and protection levels are real; an integer policy is a sequence of natural numbers read as reals. Integer-valued demand means each $X_k(\omega)$ is a natural number. Expectations are Bochner integrals.
Standing assumptions (§1). $P$ is a probability measure. The demands are measurable, nonnegative and mutually independent, and the fares are strictly decreasing.
Added hypotheses. The goal assumes positive fares, $f_k > 0$ for $k \ge 1$ . The page leaves this implicit (fares are average revenues), and without it the theorem is false. The same assumption appears in (30), and (27) assumes $f_1 \ge 0$ , without which $ER_1$ is convex rather than concave.
Derivatives. One-sided derivatives are required to exist, with their value asserted; no default value of an undefined derivative is used. The convention $\delta_- g(0) = +\infty$ is built into the subdifferential.
Optimality. Optimality is global: against every real protection-level policy, at every level $k \ge 1$ and every $s \ge 0$ .
Paper's slips corrected. (28)–(29) are stated on their range $s \ge p_k$ (resp. $s > p_k$ ). (30) is stated for every $k \ge 1$ , as the induction uses it, rather than the printed $k = 2, 3, \dots$
Not a trivialization. The goal assumes only the model, integer demand and positive fares. It does not assume concavity, CLBI, (20) or any derivative formula, and optimality is not restricted to integer competitors or to one $k$ .
Duplication. Corollary 1 and Theorem 1 are restated from the companion mission in this series.
Contributions. Proofs of the measure-theoretic derivative lemmas, of the covering property (a statement about real functions), and of the induction are all welcome.

Selected references

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1):127–137, 1993. https://doi.org/10.1287/opre.41.1.127
K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12:95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
R. E. Curry, Optimal Airline Seat Allocation with Fare Classes Nested by Origins and Destinations, Transportation Science 24(3):193–203, 1990. https://doi.org/10.1287/trsc.24.3.193
R. D. Wollmer, An Airline Seat Management Model for a Single Leg Route When Lower Fare Classes Book First, Operations Research 40(1):26–37, 1992. https://doi.org/10.1287/opre.40.1.26

Related work on the platform. The two-class, integer-capacity EMSR rule of Belobaba (1987) is formalized as SeatInventory.Nested.emsr_protection_level_optimal. It is a relative of the $k = 1$ case of Theorem 2, but it lives in a different model: two classes, a fixed integer capacity, and only integer competitors.

70 thms3 active usersReviewed

Completed

Bandit Algorithms Probability Statistics·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms I: The Nonparametric Learn-then-Price Policy Has Regret at Most C(log n)^{1/2}/n^{1/4}Research Paper

Why price without knowing demand

A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand function $\lambda(p)$ , the rate of purchase requests at price $p$ , is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.

Besbes and Zeevi (2009) asked how much revenue is lost for not knowing $\lambda$ . They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:

the problem is constrained by an initial inventory;
the set of prices is a continuum;
the set of possible demand functions is a nonparametric class.

This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order $(\log n)^{1/2}n^{-1/4}$ in a market of size $n$ .

Setting

Prices. Fix $0<\underline p<\overline p<\infty$ and an off price $p_\infty>0$ outside $[\underline p,\overline p]$ . The seller may charge any price in $[\underline p,\overline p]\cup\{p_\infty\}$ ; charging $p_\infty$ stops demand.

Demand. Requests arrive as a Poisson process whose intensity at time $t$ is $\lambda(p(t))$ . Let $N$ be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time $t$ under a price path $p(\cdot)$ are $N\big(\int_0^t\lambda(p(s))\,ds\big)$ . The seller starts with inventory $x$ and sells until either the horizon $T$ ends or the stock runs out. The expected revenue of a policy $\pi$ is $J^\pi(x,T;\lambda)$ .

Demand class. $\mathcal L=\mathcal L(M,\underline K,\overline K,m)$ is the set of regular demand functions satisfying Assumption 1. Regular means:

$\lambda\ge0$ and $\lambda(p_\infty)=0$ ;
$\lambda$ is non-increasing on $[\underline p,\overline p]$ , with inverse $\gamma$ ;
the revenue rate $r(l)=l\gamma(l)$ is concave.

Assumption 1 requires:

(i) $\lambda\le M$ on $[\underline p,\overline p]$ ;
(ii) $\lambda$ is $\overline K$ -Lipschitz and $\gamma$ is $\underline K^{-1}$ -Lipschitz;
(iii) $\max_p p\lambda(p)\ge m$ .

Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:

J^D(x,T\mid\lambda)=\sup\Big\{\int_0^T p(s)\lambda(p(s))\,ds:\int_0^T\lambda(p(s))\,ds\le x\Big\}.

The regret of a policy is $\mathcal R^\pi=1-J^\pi/J^D$ .

Scaling. In a market of size $n$ the inventory is $nx$ and the demand function is $n\lambda$ , as in (11). The corresponding quantities are $J^\pi_n$ , $J^D_n=nJ^D$ and $\mathcal R^\pi_n$ .

Algorithm 1, $\pi(\tau,\kappa)$ . The policy has three phases.

Learning. On $[0,\tau]$ it tests $\kappa$ equally spaced prices $p_i=\underline p+(i-1)(\overline p-\underline p)/\kappa$ , each for $\Delta=\tau/\kappa$ time units. It estimates $\lambda(p_i)$ by the normalized request counts $\hat\lambda(p_i)$ .
Optimization. It chooses $\hat p^u=\arg\max_i p_i\hat\lambda(p_i)$ and $\hat p^c=\arg\min_i|\hat\lambda(p_i)-x/T|$ , and sets $\hat p=\max\{\hat p^u,\hat p^c\}$ .
Pricing. It charges $\hat p$ on $(\tau,T]$ until the stock runs out.

Formalization targets

Goal: Proposition 1

Let $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ , and let $\pi_n=\pi(\tau_n,\kappa_n)$ . Then there is a finite constant $C$ , independent of $\lambda$ and $n$ , such that

\sup_{\lambda\in\mathcal L}\mathcal R^{\pi}_n(x,T;\lambda)\le\frac{C(\log n)^{1/2}}{n^{1/4}}\qquad(n\ge2).

The constant is left unspecified, as in the paper. Its dependence on the class parameters, $x$ and $T$ is "somewhat complex" (p. 12), and the order $(\log n)^{1/2}n^{-1/4}$ is the content of the result.

Milestones

The milestones follow the proof in the appendix, in order:

the scaling $J^D_n=nJ^D$ (p. 12);
Fact 1, $J^D\ge m\min\{T,x/M\}$ on $\mathcal L$ ;
Lemma 1, the solution of (5): charge $p^D=\max\{p^u,p^c\}$ until the stock runs out;
Lemma 2, a Poisson deviation bound;
the revenue lower bound (A-2);
Lemma 3, the learned price is near $p^D$ with high probability;
Lemma 4 and the Case 1 bound (A-11), for $\lambda(\overline p)\le x/T$ ;
Lemma 5 and the Case 2 bound (A-15), for $\lambda(\overline p)>x/T$ ;
the Step 4 bound $\mathcal R^\pi_n\le C_{12}(u_n+\tau_n)$ , where $u_n=(\log n)^{1/2}\max\{1/\kappa_n,(n\Delta_n)^{-1/2}\}$ .

Significance

Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order $n^{-1/2}$ for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.

The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:

a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
uniform (over the class) Poisson concentration bounds.

The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).

Difficulty

The obvious argument controls the estimation error at the tested prices and concludes that $\hat p$ is close to the optimal price. It breaks in two places.

First, $p^D$ is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at $\hat p$ is not controlled by the error in $\hat p$ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on $\gamma$ .

Second, when demand at the highest price exceeds the inventory rate ( $\lambda(\overline p)>x/T$ ), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.

Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.

Formalization scope

Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space $(\Omega,\mathbb P)$ , a published platform definition: ℕ-valued, $N(0)=0$ , monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating $N$ at cumulative intensities.
Inventory. The inventory of the market of size $n$ is $\lfloor nx\rfloor$ units, and sales are $\min\{N(\cdot),\lfloor nx\rfloor\}$ . The cap is never dropped.
Revenue. $J^\pi_n$ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
Demand functions. A demand function is a map $\mathbb R\to\mathbb R$ , nonnegative, with $\lambda(p_\infty)=0$ . Regularity and Assumption 1 are imposed on $[\underline p,\overline p]$ , and the inverse $\gamma$ is Function.invFunOn.
Benchmark. $J^D$ is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
Algorithm. The grid excludes $\overline p$ , as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare $\hat\lambda(p_i)$ with $x/T$ .
Tuning. $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ are encoded with explicit constants $0<c\le c'$ , with $\tau_n\in(0,T]$ and $\kappa_n\ge1$ . Constants may depend on $c,c'$ , the class parameters, the prices, $x$ and $T$ , but never on $\lambda$ or $n$ .
Range of $n$ . Bounds whose right side vanishes at $n=1$ because $\log1=0$ are stated for $n\ge2$ : the goal and (A-15).
Typo correction. Lemma 5's event uses $nx-C_9nu_n$ , as in its proof, not the printed $nx-C_9u_n$ .
Ruled out. A specific demand curve, a fixed $n$ , deterministic demand, a finite price set, a known $\lambda$ , constants depending on $\lambda$ , or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 ( $J^\pi\le J^D$ for all admissible policies) are not included.

Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.

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

15 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 1: A k-Fold Realizer of Size t Yields a Vertex Cover of Expected Weight at Most (2 − 2/(t/k)) Times OptimalResearch Paper

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$ -approximations for orders of fractional dimension at most $f$ . This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$ .

Two jobs $x,y$ are incomparable, $x\parallel y$ , when neither $(x,y)$ nor $(y,x)$ lies in $P$ . The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$ ; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$ . A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$ -realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$ -realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$ , and $w(C)=\sum_{u\in C}w_u$ . $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ . The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$ . For a solution $x$ write $V_a=\{u: x_u=a\}$ , and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$ .

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$ , a $k:t$ -realizer $L_1,\dots,L_t$ of $P$ , and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$ . Then every $C_i$ is a vertex cover of $G^S_P$ , and

\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.

Milestones

Proposition 3.2 (p. 657): $G^S_P=G_P$ .
Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$ .
Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$ .
Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$ .
Hochbaum's observation (§5, p. 659): for half-integral feasible $x$ , $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$ .
Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$ -approximate vertex cover of $G^S_P$ into an $\alpha$ -approximate schedule, Theorem 5.1 gives a $(2-2/f)$ -approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$ . The paper applies it to interval orders ( $3/2$ ), convex bipartite orders and semiorders ( $4/3$ ), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$ -fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$ .

Formalization scope

Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
$\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$ -realizer is a family Fin t → LinearExtension P with $t>0$ . Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's " $y>x$ " in Eq. (4) and " $\mathrm{Prob}[j>i]$ " in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
$G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
[CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ , taken over a finite nonempty family.
Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$ , which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$ . The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$ .
Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$ , and equals $2$ when $k=0$ .
The paper assumes $\operatorname{fdim}(P)\ge2$ , i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$ .
Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

10 thms3 active usersReviewed

Completed

Convex Optimization Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization V: The Order-Statistic Box U^M Built from Marginal Samples Dominates Value at Risk with Probability at Least 1 − αResearch Paper

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$ . The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$ .

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$ , observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$ . Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$ .

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$ . A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$ , $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$ .

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$ , $1\le j\le N$ , be the $j$ -th order statistic (the $j$ -th smallest value) of coordinate $i$ , and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}

and the uncertainty set is the box

\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$ .

Formalization targets

Goal: Theorem 7

If $N-s+1<s$ , then with probability at least $1-\alpha$ over the sample ( $N$ samples of each marginal of $\mathbb P^*$ , each marginal's samples i.i.d., arbitrary dependence across marginals),

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}

Milestones

Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
Each one-sided order-statistic test is valid at level $\alpha/(2d)$ : $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$ , and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
(EC.8): for $\mathbb P\in\mathcal P^M$ , $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
(29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$ , so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$ , where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$ , where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$ , and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$ , a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$ .

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$ -th sample of marginal $i$ , under any probability law Q such that, for each $i$ , the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$ -th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$ , together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$ . Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$ . A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$ , $0<\epsilon<1$ , $0<\alpha<1$ , $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$ , $\mathbb P^*$ a probability measure with $\mathbb P^*$ -null complement of the box, and Theorem 7's hypothesis $N-s+1<s$ . The page prints the second condition of $\mathcal P^M$ as " $\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$ "; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with " $\le$ " for each $\mathbb P\in\mathcal P^M$ ; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

11 thms3 active usersReviewed

Completed

Convex Optimization Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization IV: The Forward–Backward Deviation Set U^FB Has a Closed-Form Support Function That Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$ .

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$ , the Value at Risk is

\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$ , the forward deviation and the backward deviation are

\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.

From a sample, a bootstrap produces thresholds $t_i$ , $\bar\sigma_{fi}$ , $\bar\sigma_{bi}$ . With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$ . The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$ , each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$ , $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$ .

The uncertainty set is

\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$ , $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$ , the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)

for every $v$ , and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$ .

Milestones

The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$ .
The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$ .
Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$ .
The three one-dimensional sub-subproblems and their optimal values.
The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$ .
$\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$ , attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$ .

Companions

Remark 9: when (24) exceeds $t$ , an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$ .
Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$ .

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$ , which should be $v_i^2\bar\sigma^2/(2\lambda)$ , and the bound $m_b\le y_1\le m_b$ ). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$ . The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$ , and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$ , so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

$\bar\sigma_{fi},\bar\sigma_{bi}>0$ , so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$ .
$m_b\le m_f$ , which holds because $t_i\ge0$ .
The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
" $\sigma_f(\mathbb P_i)\le\bar\sigma$ " is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$ ", which is equivalent and avoids an unbounded supremum.
Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$ , stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$ .

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

12 thms3 active usersReviewed

Completed

Convex Optimization Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization III: For Independent Marginals, the Kolmogorov–Smirnov Set U^I Has Support Function (19) and Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$ , and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$ . The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$ -th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$ .

The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$ .
The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$ .
The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$ .
The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$ .
The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$ , $q^L$ puts mass $\Gamma$ at $j=0$ , mass $1/N$ at $j=1,\dots,k$ , and mass $1-\Gamma-k/N$ at $j=k+1$ . Its mirror image is $q^R_j=q^L_{N+1-j}$ .
The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$ .
The uncertainty set (18) is

\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$ :

\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,

\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}

Milestones, in attack order

The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
The boundary laws $q^L$ , $q^R$ belong to $\mathcal P^{KS}_i$ .
Theorem EC.2: for monotone $g$ , $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$ .
(16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$ .
The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$ .
(EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$ .
(EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

worst-case expectations over a KS confidence band;
the finite Gibbs variational identity with possibly vanishing reference masses;
a Chernoff-type Value-at-Risk bound for product measures;
a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$ , which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$ , and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$ , and the KS constraints run over j : Fin N, which is the page's $j-1$ . The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
Standing assumptions. $N\ge1$ , $0<\Gamma<1$ and $0<\epsilon<1$ .
Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
Relative entropy. $D$ carries an explicit finiteness predicate ( $q_j>0\Rightarrow p_j>0$ ), so Lean's log 0 = 0 cannot make an infinite divergence finite.
Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ , and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$ . By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$ . It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$ . This part is cited, not formalized.
Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$ , and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$ .

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

11 thms3 active usersReviewed

Completed

Combinatorics Linear algebra·Captain: mikedeng1

On the Abstract Properties of Linear Dependence 4: Orthogonal Subspaces Have Dual MatroidsResearch Paper

Motivation

Hassler Whitney introduced matroids in On the Abstract Properties of Linear Dependence (Amer. J. Math. 57, 1935, doi:10.2307/2371182) to capture what linear dependence among the columns of a matrix and the circuit structure of a graph have in common. One of the central constructions of the paper is duality. For graphs, duality exists only for planar graphs (Whitney, Non-separable and planar graphs, Trans. AMS 34, 1932); for matroids Whitney showed that every matroid has a dual, and that duality has a direct linear-algebra model: the matroid of a subspace of $\mathbb R^n$ and the matroid of its orthogonal complement are duals.

Matroid duality underlies much of combinatorial optimization: the duality between cycles and cuts in graphs, the relation between a linear code and its dual code, the exchange of rank and corank in matroid intersection and partition, and the treatment of network flows as duals of potential problems. Whitney's §§11–13 are where this structure is first defined and where its linear-algebra meaning (Theorem 28) is established.

Setting

A matroid $M$ is a finite set of elements $e_1,\dots,e_n$ with a rank function $r$ on its subsets; equivalently, a family of independent sets, or of bases (maximal independent sets). For a subset $N$ write $\rho(N)$ for its number of elements and

n(N) = \rho(N) - r(N)

for its nullity; $r(M)$ and $n(M)$ are the rank and nullity of the whole set of elements.

Duality (§11). Let $M$ and $M'$ be matroids and $\sigma$ a one-to-one correspondence between their elements. $M'$ is a dual of $M$ (via $\sigma$ ) if, for every subset $N$ of $M$ , with $N'$ the complement in $M'$ of $\sigma(N)$ ,

r(N') = r(M') - n(N). \tag{11.1}

The matroid of a subspace (§12). Let $E_n$ be $n$ -dimensional Euclidean space with coordinates $x_1,\dots,x_n$ , and let $H$ be a hyperplane through the origin, which in Whitney's usage is a linear subspace of any dimension. For a set $S$ of coordinates, project $H$ onto the coordinate subspace $E'_S$ spanned by the axes $x_i$ , $i\in S$ . The matroid associated with $H$ has elements $e_1,\dots,e_n$ , one per coordinate, and gives the set $\{e_i: i\in S\}$ the rank

r_H(S) = \dim \pi_S(H).

If $H$ is the row space of a matrix $\mathbf M$ , then $r_H(S)$ is the rank of the columns of $\mathbf M$ indexed by $S$ , so the associated matroid is the column matroid of $\mathbf M$ .

In the Lean development these objects are WhitneyMatroid.Components.nullity (shared), IsDualVia M M' σ, IsDual M M', subspaceRank H S and IsAssociated M H.

Formalization targets

Goal: Theorem 28

Let $H$ be a subspace of $E_n$ and $H' = H^\perp$ its orthogonal complement. If $M$ and $M'$ are the matroids associated with $H$ and $H'$ , then $M$ and $M'$ are duals under the correspondence of equal coordinates:

\forall N\subseteq\{e_1,\dots,e_n\}:\qquad r_{M'}(\overline N) = r(M') - n_M(N).

Milestones

Theorem 27. For every subspace $H$ there is exactly one matroid associated with $H$ .
Theorem 6 (already proved on the platform). All bases have the same number of elements.
Theorem 7. $B$ is a base iff $r(B)=r(M)$ and $n(B)=0$ .
Theorem 8. If $B$ is a base and $N$ is independent, then $N\cup N'$ is a base for some $N'\subseteq B$ .
Theorem 20. If $M'$ is a dual of $M$ , then $r(M') = n(M)$ and $n(M') = r(M)$ .
Theorem 23. $M'$ is a dual of $M$ via $\sigma$ iff, for every $B$ , $B$ is a base of $M$ exactly when the complement of $\sigma(B)$ is a base of $M'$ .
Theorem 21. Duality is symmetric.
Theorem 22. Every matroid has a dual.

Significance

The result. Theorem 28 identifies abstract duality with orthogonal complementation. With Theorem 23 it says that the column matroid of a real matrix whose rows span $H$ and the column matroid of a matrix whose rows span $H^\perp$ have complementary bases. This is the basis of the standard representation of the dual of a represented matroid ( $[I_r\mid A]$ and $[-A^{\mathsf T}\mid I_{n-r}]$ ), of the cycle/cocycle duality of graphs viewed through incidence matrices, and of the fact that a matroid representable over a field has a dual representable over the same field. Theorems 20–23 are the basic facts every later treatment of matroid duality starts from: duality exchanges rank and nullity, is symmetric, always exists, and is characterized by base complements.

Formalizing it. All of these results are classical and proved in Whitney's paper; what this mission adds is a machine-checked development of Whitney's own definition of duality, the rank identity (11.1), rather than the base-complement definition used in modern libraries. Mathlib defines the dual matroid $M^*$ by base complements and proves that it is a matroid; it does not, at the pinned revision, contain the rank formula (11.1) for $M^*$ , the matroid of a real subspace, or Theorem 28. Theorem 6 is already proved on the platform and enters as a reference. Theorems 7 and 8 are close to Mathlib lemmas and are footholds rather than new content.

Difficulty

The difficulty of the goal is not in the combinatorics but in the passage between the two descriptions of a subspace. The natural first idea is to compare the ranks $r_H(S)$ and $r_{H^\perp}(\overline S)$ directly by counting dimensions of $H$ and $H^\perp$ . This does not close: $r_H(S)$ is the dimension of a projection of $H$ onto coordinates, while $\dim H^\perp = n - \dim H$ only controls $H^\perp$ as a whole, and the rank of a complementary coordinate set in $M'$ is not determined by the dimensions of $H$ and $H^\perp$ alone. Some relation between coordinate projections of $H$ and the structure of $H^\perp$ on the complementary coordinates has to be established. Theorem 27 is itself nontrivial in Lean: the rank function $r_H$ has to be shown to satisfy the matroid axioms, which needs a careful treatment of coordinate projections and of submodularity of dimension. On the abstract side, Theorem 23 needs both directions of the passage between the rank identity and base complements, including the counting step $r(M) + r(M') = \rho(M)$ .

Formalization scope

Matroids are Mathlib Matroid α on a finite type α whose ground set is all of α (Whitney's matroid is its finite set of elements). This finiteness and the ground set convention are part of the definitions; all theorems are stated under them.
Ranks and nullities. Ranks are Mathlib's eRk, finite on a finite type and converted to integers; the nullity $n(N)=\rho(N)-r(N)$ and the identity (11.1) are computed in $\mathbb Z$ . No truncated subtraction appears.
Duality is Whitney's rank identity (11.1) for every subset, for a fixed bijection σ : α ≃ β (IsDualVia) or some bijection (IsDual). It is deliberately not defined as Mathlib's M✶: with that definition Theorem 23 would be nearly definitional and Theorem 28 would lose the rank identity. A formalization that replaces (11.1) by the base-complement condition, or states Theorem 28 only for bases, is not this mission's goal.
Euclidean space is EuclideanSpace ℝ (Fin n) with its standard inner product; the orthogonal hyperplane is Hᗮ. The field is $\mathbb R$ , as in the paper; the analogous statement over other fields with the dot-product annihilator is a generalization and not part of this mission.
The associated matroid is a predicate (IsAssociated M H): ground set Fin n, and the rank of every set $S$ of coordinates equals the finrank of the image of $H$ under the coordinate projection onto $S$ (not of $H\cap E'_S$ , a different set function). Existence and uniqueness is Theorem 27.
Implicit hypotheses made explicit: the ground sets are finite and equal to the whole element type; Whitney's "dimension $r$ " and "dimension $n-r$ " in Theorem 28 are consequences of $H'=H^\perp$ and are not hypotheses. The goal covers $n=0$ , $H=\{0\}$ and $H=E_n$ .
Infrastructure needed and reusable: the matroid of a real subspace (equivalently the column matroid of a real matrix), with its rank function in terms of coordinate projections; the rank formula of the dual matroid; the dimension identity relating projections of $H$ and sections of $H^\perp$ . All are reusable for the other missions of this series (the Fano matroid and binary matroids) and for any later work on represented matroids. Proofs of the milestones, alternative proofs of Theorem 28 through Mathlib's M✶, and supporting lemmas on coordinate projections are welcome.

Selected references

H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011, Chapter 2 (duality). https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
Mathlib, Mathlib.Combinatorics.Matroid (Dual, Rank). https://github.com/leanprover-community/mathlib4

12 thms3 active usersReviewed

Completed

Probability·Captain: mikedeng1

Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model 3: A Closed Form for the Induced Penalty Cost under Normal DemandResearch Paper

Motivation

Multiechelon inventory theory studies supply systems in which stock is held at several levels: here, a depot that orders from an outside supplier and a retail outlet that is replenished from the depot and faces random customer demand. The question is how much to order and ship in each period so as to minimize expected holding, shortage and ordering costs over an infinite horizon. Clark and Scarf (Management Science, 1960) showed that the finite-horizon problem of a serial system decomposes into single-location problems linked by an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) extended the decomposition to the infinite horizon under discounted and average costs, and then asked what it costs to compute an optimal policy.

In the reduced single-location problem the only nonlinear part of the one-period cost is the expected induced penalty $P^L$ . Any algorithm for the reduced problem (Veinott–Wagner type policy computations, for instance) evaluates $P^L$ many times. In general each evaluation is a numerical integral. Section 4 of the paper shows that when demand is normal, $P^L$ has a closed form in the univariate and bivariate standard normal distribution functions. This mission formalizes that closed form, eq. (13) on p. 830.

Setting

Time is discrete. One-period demand is $u\sim N(\mu,\sigma^2)$ with $\sigma>0$ , independent across periods. For $i\ge1$ , $u^{(i)}$ is the total demand over $i$ periods. It is normal with mean $\mu^{(i)}=i\mu$ and standard deviation $\sigma^{(i)}=i^{1/2}\sigma$ , density $f^{(i)}$ and cdf $F^{(i)}$ . The shipment lead time from depot to outlet is $l\ge0$ and the order lead time from the supplier is $L\ge1$ . The cost factors are a system-wide holding cost $h^d>0$ , a retailer holding cost $h^r>0$ and a retailer shortage penalty $p^r>0$ . Write $p^s=h^d+p^r$ . Costs are average costs, so the discount factor is $\alpha=1$ throughout.

The retailer's one-period cost (p. 822) is

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

The critical number $x^{r*}$ is a global minimizer of $R$ (property (b), p. 824). The induced penalty cost is $P(x)=0$ for $x\ge x^{r*}$ and $P(x)=R(x)-R(x^{r*})$ for $x<x^{r*}$ . Its expectation over the order lead time is

P^L(x)=E\,P[x-u^{(L)}]\qquad\text{(eq. (10))}.

Let $\Phi$ and $\phi$ be the standard normal cdf and density, $\Theta(z)=z\Phi(z)+\phi(z)$ , and $\Phi(\xi_1,\xi_2;\rho)$ the cdf of a bivariate normal pair with standard normal marginals and correlation $\rho$ . The paper defines (p. 830)

\tau_1(x)=-\frac{x-(x^{r*}+\mu^{(L)})}{\sigma^{(L)}},\quad \tau_2(x)=\frac{x-\mu^{(L+l+1)}}{\sigma^{(L+l+1)}},\quad \nu^{r*}=\frac{x^{r*}-\mu^{(l+1)}}{\sigma^{(l+1)}},

\tau_3(x)=-\frac{x-(x^{r*}+\mu^{(L)})-[\sigma^{(L)}/\sigma^{(l+1)}]^2[x^{r*}-\mu^{(l+1)}]}{\sigma^{(L)}\sigma^{(L+l+1)}/\sigma^{(l+1)}},

\epsilon_1(x)=\frac{\Phi[\tau_3(x)]\phi[\tau_2(x)]}{\sigma^{(L+l+1)}},\qquad \epsilon_2(x)=\frac{\Phi(\nu^{r*})\phi[\tau_1(x)]}{\sigma^{(L)}},\qquad \iota(x)=\sigma^{(L)}\Theta[\tau_1(x)],

\kappa(x)=\sigma^{(l+1)}\Theta(\nu^{r*})\Phi[\tau_1(x)]-\{[\sigma^{(L+l+1)}]^2\epsilon_1(x)-[\sigma^{(L)}]^2\epsilon_2(x)\}-[x-\mu^{(L+l+1)}]\,\Phi[\tau_1(x),\tau_2(x);\rho],

with $\rho=-\sigma^{(L)}/\sigma^{(L+l+1)}$ .

Formalization targets

Goal: eq. (13)

For every real $x$ ,

P^L(x)=p^s\,\iota(x)-(p^s+h^r)\,\kappa(x).

This is an exact identity for every admissible parameter value. It holds with no constants left free.

Milestones

The milestones follow the paper's outline of the derivation on pp. 829–831:

eq. (11), $R(x)=p^s[\mu^{(l+1)}-x]+(p^s+h^r)\int_{-\infty}^xF^{(l+1)}(t)\,dt-h^d\mu$ ;
eq. (12), $P^L(x)=\int_{x-x^{r*}}^\infty[R(x-t)-R(x^{r*})]f^{(L)}(t)\,dt$ ;
eq. (14), $P^{L\prime}(x)=-p^s\Phi[\tau_1(x)]+(p^s+h^r)\int_{x-x^{r*}}^\infty F^{(l+1)}(x-t)f^{(L)}(t)\,dt$ ;
eq. (15), the same derivative with the integral replaced by $\Phi[\tau_1(x),\tau_2(x);\rho]$ ;
$P^L(x)\to0$ as $x\to\infty$ , hence $P^L(x)=-\int_x^\infty P^{L\prime}(t)\,dt$ ;
$\iota'(x)=-\Phi[\tau_1(x)]$ and $\iota(x)\to0$ ;
the two conditional-normal identities, which give $\Phi[\tau_3(x)]$ and $\Phi(\nu^{r*})$ ;
$\frac{d}{dx}\Phi[\tau_1(x),\tau_2(x);\rho]=\epsilon_1(x)-\epsilon_2(x)$ ;
and 10. the formulas for $\epsilon_1'$ and $\epsilon_2'$ ;
$\kappa'(x)=-\Phi[\tau_1(x),\tau_2(x);\rho]$ and $\kappa(x)\to0$ .

Two side remarks of p. 830 are also included: $\Theta'=\Phi$ , and the simplified form of $\tau_3$ .

Significance

The result. Under normal demand, (13) replaces the numerical integral (12) with a few evaluations of $\Phi$ , $\phi$ and the bivariate normal cdf, all available in standard numerical libraries. Together with the decomposition results of Sections 1–3 of the paper, it makes the policy computation for the two-echelon system with normal demand no harder than a single-location computation with an explicit cost function. The same functions reappear in the paper's Section 5 for several retail outlets, after a reinterpretation of $\sigma^{(l+1)}$ .

Formalizing it. The paper proves (13) only in outline: it calls the derivation "an elementary integration problem, but … sufficiently involved to warrant an outline" and leaves "tedious algebra" and "more algebra" to the reader. A machine-checked proof turns that outline into a complete argument, including the analytic steps the outline passes over: differentiation under the integral sign, the limits at $+\infty$ , and the identification of an integral of normal densities with a bivariate normal probability. To our knowledge no formal proof of (13) exists, and no bivariate normal distribution function is on the platform yet.

Difficulty

The obvious approach is to substitute (11) into (12) and integrate. The result is a double integral of normal densities over a region bounded by a line, and it does not reduce to univariate functions. The paper's route is to differentiate first, identify the derivative (14) as a probability for the correlated pair $(u^{(L)},u^{(L)}+u^{(l+1)})$ , and then recover $P^L$ by integrating from $+\infty$ . That route needs three things: justification for differentiating under the integral in (12), whose integrand has a kink at $t=x-x^{r*}$ ; control of the limits at $+\infty$ ; and the conditional-normal identities, which involve conditioning on a null event and so must be handled through densities. The verification of $\kappa'$ is a long computation with $\Theta$ , $\epsilon_1$ and $\epsilon_2$ , in which every constant matters.

Formalization scope

Everything lives in the namespace FZEchelon.NormalDemand. The model data form the structure Data (fields $\mu,\sigma,h^d,h^r,p^r,l,L,x^{r*}$ ). The law of $u^{(i)}$ is the platform's normal demand law InventoryControl.newsboyDemand with mean $i\mu$ and standard deviation $\sqrt i\,\sigma$ . Expectations are Bochner integrals, and improper integrals are set integrals over Set.Ioi/Set.Iic. $\Phi$ is cdf (gaussianReal 0 1). The bivariate cdf is the iterated integral of the explicit bivariate density over a lower-left quadrant (meaningful for $|\rho|<1$ ; here $\rho\in(-1,0)$ ). Derivatives are HasDerivAt and limits are Tendsto … atTop (𝓝 0).

Standing hypotheses of every theorem: $\sigma>0$ ; $h^d,h^r,p^r>0$ (p. 821); $L\ge1$ ; and $x^{r*}$ minimizes $R$ . Two of these are added to the page and disclosed. $\sigma>0$ is needed because every $\tau$ divides by some $\sigma^{(i)}$ . $L\ge1$ is needed because $\sigma^{(0)}=0$ , and the paper treats zero order lead time separately (p. 819). Demand is exactly normal, as in §4, which acknowledges that this violates $u\ge0$ and ignores the objection. No nonnegativity, truncation or approximation enters. The goal fixes $\alpha=1$ , the average-cost case the section restricts to. The discounted analogue is not part of this mission.

A trivializing formalization is ruled out: every Bochner integral in the statements has an integrable integrand, since integrands grow at most linearly and the normal law has all moments. No division by a zero standard deviation can occur under the hypotheses. A sorry-free check in the workspace shows that all hypotheses hold together, with a minimizer $x^{r*}$ of $R$ proved to exist.

Needed infrastructure: properties of gaussianReal (moments, convolution of independent normals), differentiation of parametric integrals, and a bivariate normal distribution function with its partial derivatives. A reusable treatment of the bivariate normal cdf, linking the density form used here to Mathlib's multivariateGaussian, would be a contribution of independent value. Proofs of individual milestones are welcome in any order.

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
A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525

17 thms3 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

Contraction Mappings in the Theory Underlying Dynamic Programming 1: Under the Contraction and Monotonicity Assumptions the Solution of the Functional Equation Is the Optimal ReturnResearch Paper

Why this problem arose

Dynamic programming often replaces a search over whole plans with an equation for a value function. That replacement is useful only when solving the equation recovers the value actually available through policies. In his 1967 paper, Eric Denardo isolated conditions on an abstract return function that make this identification possible, without committing to a particular transition law or a finite state space. The framework covers discounted decision models and other examples discussed in the paper, while allowing different decisions at different states. Denardo, 1967.

The mission concerns the paper's first regime: a one-step contraction together with monotonicity. It focuses on the question raised just after equation (4): does the solution of the functional equation equal the supremum of the return functions generated by policies? The paper proves that it does under these assumptions. Its later $N$ -stage regime is a separate mission. Denardo, 1967, pp. 167–169.

States, decisions, and returns

Let $\Omega$ be a set of states. At each $x\in\Omega$ there is a decision set $D_x$ . A policy $\delta$ selects a decision $\delta_x\in D_x$ at every state, so the policy space $\Delta$ is the full Cartesian product $\prod_{x\in\Omega}D_x$ . Let $V$ be the bounded real functions on $\Omega$ , with the uniform metric $\rho(u,v)=\sup_{x\in\Omega}|u(x)-v(x)|$ . A return function $h(x,d,v)$ assigns a real return to a state, an available decision, and a continuation value $v\in V$ . Denardo, 1967, p. 166.

For a policy $\delta$ , its policy operator $H_\delta$ acts by $(H_\delta v)(x)=h(x,\delta_x,v)$ . Under the contraction assumption, some $c$ satisfies $0\le c<1$ and $|h(x,d,u)-h(x,d,v)|\le c\rho(u,v)$ for all eligible $x,d,u,v$ . Each $H_\delta$ then has a unique fixed point $v_\delta\in V$ , called that policy's return function. The optimal return function is defined pointwise by $f(x)=\sup_{\delta\in\Delta}v_\delta(x)$ . These are the paper's definitions, rather than a presumed equality between $f$ and a Bellman fixed point. Denardo, 1967, pp. 166–167.

The maximization operator $A$ instead chooses the best decision at each state for a supplied continuation value: $(Av)(x)=\sup_{d\in D_x}h(x,d,v)$ . Denardo assumes that $H_\delta v$ and $Av$ remain bounded, so both operators act on $V$ . The monotonicity assumption says that $u\ge v$ pointwise implies $H_\delta u\ge H_\delta v$ for every policy. These are separate conditions: contraction controls distance between value functions, while monotonicity controls their order. Denardo, 1967, pp. 166–168.

Formalization targets

The central target is Theorem 3. Under contraction and monotonicity, the unique bounded solution $v^*$ of equation (4) is the optimal return:

Av^*=v^*,\qquad v^*(x)=f(x)=\sup_{\delta\in\Delta}v_\delta(x)\quad(x\in\Omega).

The milestones follow the paper's route to that assertion. Theorem 1 bounds a policy's return by its fixed-point residual, $\rho(v_\delta,w)\le\rho(H_\delta w,w)/(1-c)$ . Theorem 2 says that $A$ itself has modulus at most $c$ . The text accompanying equation (4) establishes that $A$ has exactly one fixed point. Corollary 1 then gives, for each $\varepsilon>0$ , a policy with residual at most $\varepsilon(1-c)$ at that fixed point and return within $\varepsilon$ of it, together with an exact equality criterion for zero residual. Denardo, 1967, pp. 167–168.

What the result gives

Theorem 3 justifies reading the functional equation as an optimization equation: its solution is the pointwise supremum of returns realized by the paper's policy model. Corollary 1 supplies policy returns arbitrarily close to that solution in the uniform metric. With the compactness and continuity assumptions of Corollary 2, the paper also obtains a policy that attains it, though that optional result is outside this mission's milestone list. Denardo, 1967, pp. 167–168.

The mathematical result was proved in the cited paper. This mission asks for machine-checked proofs of its abstract statements in Lean, including the residual estimate, the maximization operator's contraction, fixed-point existence, and the identification with optimal policy return. The definitions are reusable for decision models whose returns fit Denardo's assumptions; they do not prescribe a probability kernel or a finite action set.

Where the difficulty lies

The fixed-point theorem alone identifies a unique solution of $Av=v$ ; it does not identify that solution with $f$ , because $f$ is defined through the separate fixed points of all $H_\delta$ . The distinction matters: the paper observes that contraction without monotonicity can leave $v^*$ different from $f$ , and gives $h(x,d,v)=-v(x)/2$ as a nonmonotone example. The formal goal therefore retains both definitions and requires monotonicity. Denardo, 1967, pp. 167–168.

There is also a choice issue in Corollary 1. A near-maximizing decision is available separately at every state, while its conclusion asks for one policy choosing all those decisions at once. The full Cartesian policy space is essential to the statement. On an infinite state set, the value functions must remain bounded even after applying $A$ or a policy operator; contraction of differences by itself does not provide that range condition. Denardo, 1967, pp. 166–168.

Formalization scope

Lean represents $V$ by bounded real functions lp (fun _ : Ω => ℝ) ⊤; its metric is $\rho$ . The state type may be infinite or empty, and decision sets depend on the state. Policies are precisely dependent functions $\delta:(x:\Omega)\to D_x$ . The operators $H_\delta$ and $A$ are maps into $V$ supplied with equations fixing their values from $h$ . This expresses the bounded-range assumptions on pages 166–167. Pointwise order is explicit because the bounded-function type has no order instance. Denardo, 1967, pp. 166–168.

Every supremum in the mission is a genuine real least upper bound. IsMaxOperator requires it for the decision returns at each state; IsOptimalReturn requires it for the policy returns. These predicates avoid assigning a default value to an empty or unbounded supremum. Where states exist, IsMaxOperator also entails a nonempty decision set. The family $v_\delta$ is supplied with $H_\delta v_\delta=v_\delta$ ; contraction ensures each such return exists uniquely. Equation (4) and the main goal explicitly assert existence of the fixed point of $A$ , so the goal cannot hold merely because there is no solution to identify. Defining $f$ from the fixed point of $A$ , or defining $v^*$ from the policy supremum, would erase the paper's substantive claim and is excluded.

The definition layer needs bounded functions, uniform distance, real least upper bounds, and dependent policies. The theorem layer needs fixed-point and order reasoning on these objects. Contributions toward those general operator facts and the paper's four milestone statements are within scope.

Selected references

Eric V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2), 165–177, 1967. DOI: 10.1137/1009030.

6 thms3 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Assortment Optimization under Variants of the Nested Logit Model 4: With Dissimilarity Parameters at Most One, the Knapsack-Relaxation and Singleton LP Optimum Scaled by 2 Is Feasible for the Full LPResearch Paper

Motivation

Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.

When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.

Setting

There are $m$ nests $M$ and, in each nest, $n$ products $N = \{1, \dots, n\}$ . Product $j$ of nest $i$ has a revenue $r_{ij} \ge 0$ and a preference weight $v_{ij} > 0$ , with $r_{i1} \ge \dots \ge r_{in}$ . Nest $i$ has a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$ ; $v_0 \ge 0$ is the weight of choosing no nest. For an assortment $S_i \subseteq N$ ,

V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)},\quad R_i(\emptyset)=0,

and the expected revenue of $(S_1, \dots, S_m)$ is $\Pi = \sum_i V_i(S_i)^{\gamma_i} R_i(S_i) / (v_0 + \sum_i V_i(S_i)^{\gamma_i})$ . The optimal expected revenue $Z^*$ is the optimal value of the linear program

\text{(3)}\quad \min\ x \quad\text{s.t.}\quad v_0 x \ge \sum_{i \in M} y_i,\qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big)\ \ \forall S_i \subseteq N,\ i \in M,

and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.

Throughout, $\gamma_i \le 1$ for every nest and the $v_{i0}$ are arbitrary. For a capacity $\epsilon_i \ge 0$ , the knapsack value $K_i(\epsilon_i)$ is the largest $\sum_{j \in S} r_{ij} v_{ij}$ over assortments $S$ with $\sum_{j \in S} v_{ij} \le \epsilon_i$ (display (9)). Its continuous relaxation (11) allows fractional $z_{ij} \in [0, \mathbf 1(v_{ij} \le \epsilon_i)]$ under the same capacity. The greedy solution $\hat z_i(\epsilon_i)$ of (11) fills the capacity with the products of weight at most $\epsilon_i$ in revenue order, each fully while it fits and the next one fractionally, and

\hat S_i(\epsilon_i) = \{ j \in N : \hat z_{ij}(\epsilon_i) = 1 \}.

Problem (10) replaces the per-assortment constraints of (3) by $y_i \ge \max_{\epsilon_i \ge 0} (v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$ .

Formalization targets

Goal: Theorem 10 (p. 24)

Let $(\hat x, \hat y)$ be an optimal solution of (4) with candidate collections $\{\hat S_i(\epsilon_i) : \epsilon_i \in [0,\infty]\} \cup \{\{j\} : j \in N\}$ . Then

(2\hat x,\ 2\hat y) \ \text{ is feasible for (3).}

Milestones

Per-nest identity (proof of Lemma 9, p. 23). For $x \ge 0$ , $\max_{S_i} V_i(S_i)^{\gamma_i}(R_i(S_i) - x) = \max_{\epsilon_i \ge 0}(v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$ .
Lemma 9 (p. 23). Problems (3) and (10) have the same optimal solutions.
Relaxation (p. 23). Every feasible point of (9) is feasible for (11), so $\hat K_i(\epsilon_i) \ge K_i(\epsilon_i)$ .
Greedy solution (pp. 23–24). $\hat z_i(\epsilon_i)$ is optimal for (11) and has at most one fractional component.
Sign (A.3, p. 45). $\hat x \ge 0$ .
Inequalities (28) and (29) (A.3, pp. 45–46). In both cases — $\hat z_i(\epsilon)$ with and without a fractional component — $2\hat y_i \ge (v_{i0}+\epsilon)^{\gamma_i}[K_i(\epsilon)/(v_{i0}+\epsilon) - 2\hat x]$ .

Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every $\hat S_i(\epsilon_i)$ is one of the at most $1 + n^2$ assortments $N^k_{ij}$ , the first $j$ products by revenue among the $k$ lightest.

Significance

Theorem 10 turns an NP-hard assortment problem into a linear program with $1 + m$ variables and $1 + m(1 + n + n^2)$ constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).

The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.

Difficulty

The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using $\gamma_i \le 1$ and $x \ge 0$ in an essential way. The second obstacle is that the greedy assortment $\hat S_i(\epsilon_i)$ keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.

Formalization scope

Products are Fin n (indices $0, \dots, n-1$ ), nests a finite type, and every quantity is real. Powers are Real.rpow; $x/0 = 0$ , which gives $R_i(\emptyset) = 0$ . An optimal solution of a linear program is a feasible pair whose $x$ is minimal among feasible pairs. The constraint " $y_i \ge \max_{\epsilon_i \ge 0}(\dots)$ " of (10) is stated in constraint form, for every $\epsilon_i \ge 0$ , so no real supremum is taken. $K_i(\epsilon)$ is defined for $\epsilon \ge 0$ only; its placeholder value for $\epsilon < 0$ is never used. Ties in revenue (and, for $N^k_{ij}$ , in weight) are broken by index. The candidate collection is taken over real $\epsilon_i \ge 0$ ; $\epsilon_i = \infty$ adds nothing, since every capacity of at least $\sum_j v_{ij}$ already gives $\hat S_i = N$ .

Standing assumptions and added hypotheses: $\gamma_i \le 1$ for every nest (the section's assumption) on the goal and on every model milestone; the pins $v_{ij} > 0$ , $r_{ij} \ge 0$ , $\gamma_i > 0$ and the revenue ordering, shared by the series; $n \ge 1$ on Lemma 9, on $\hat x \ge 0$ and on (28)/(29), the paper's nonempty $N$ ; and $v_0 > 0$ on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.

The greedy assortments $\hat S_i(\epsilon_i)$ are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.

Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of $t \mapsto t^{\gamma}$ and $t \mapsto t^{\gamma - 1}$ for $\gamma \le 1$ , and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

Selected references

J. M. Davis, G. Gallego, H. Topaloglu, Assortment Optimization under Variants of the Nested Logit Model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). DOI 10.1287/opre.2014.1256
K. T. Talluri, G. J. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 15–33, 2004. DOI 10.1287/mnsc.1030.0147
D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. DOI 10.1017/CBO9780511921735

11 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Assortment Optimization under Variants of the Nested Logit Model 2: With Dissimilarity Parameters at Most One and Fully-Captured Nests, a Nested-by-Revenue Assortment in Every Nest Is OptimalResearch Paper

Motivation

A retailer choosing which products to display, or an airline choosing which fare classes to open, solves an assortment optimization problem: pick the set of offered products that maximizes expected revenue when customers choose among what is offered according to a discrete choice model. Under the multinomial logit model the answer has a simple form: an optimal assortment consists of the few highest-revenue products (Talluri and van Ryzin, 2004). The multinomial logit model, however, forces every pair of products to compete in the same way. The nested logit model relaxes this by grouping products into nests (brands, store sections, departure times) and letting a customer first choose a nest and then a product inside it.

Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) study how much of the multinomial logit structure survives under the nested logit model. Their first answer is the theorem this mission targets: when the nest dissimilarity parameters are at most one and no customer who chose a nest leaves it without buying, offering the top products of each nest is still optimal. The other missions of this series treat the cases where this fails: dissimilarity parameters above one (the problem becomes NP-hard) and nests with their own no-purchase option.

Setting

There are $m$ nests $M = \{1, \dots, m\}$ and, in each nest, $n$ products $N = \{1, \dots, n\}$ . Product $j$ of nest $i$ has a revenue $r_{ij} \ge 0$ and a preference weight $v_{ij} > 0$ ; products are ordered so that $r_{i1} \ge r_{i2} \ge \dots \ge r_{in}$ . Nest $i$ carries a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$ , and $v_0 \ge 0$ is the weight of choosing no nest at all.

An assortment is a tuple $(S_1, \dots, S_m)$ of subsets $S_i \subseteq N$ . Write

V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \quad R_i(\emptyset) = 0.

A customer picks nest $i$ with probability $Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l \in M} V_l(S_l)^{\gamma_l})$ and then, inside the nest, product $j$ with probability $v_{ij}/V_i(S_i)$ . The expected revenue is

\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i\, R_i(S_i) = \frac{\sum_{i \in M} V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_{i \in M} V_i(S_i)^{\gamma_i}},

and problem (2) asks for $Z^* = \max \Pi(S_1, \dots, S_m)$ over all assortments. The nested-by-revenue assortment $N_{ij} = \{1, \dots, j\}$ collects the $j$ highest-revenue products of nest $i$ , with $N_{i0} = \emptyset$ and $N_+ = \{0, 1, \dots, n\}$ .

This mission works under the standing assumptions of §3 of the paper: competitive products, $\gamma_i \le 1$ , and fully-captured nests, $v_{i0} = 0$ , for every nest $i$ .

Formalization targets

Goal: Theorem 4 (p. 15)

If $\gamma_i \le 1$ and $v_{i0} = 0$ for all $i \in M$ , there exists an optimal solution $(S^*_1, \dots, S^*_m)$ of problem (2) such that

S^*_i = N_{ij} \ \text{ for some } j \in N_+, \qquad \text{for all } i \in M.

Milestones

The case $v_0 = 0$ (p. 14). Offering only the single product with the largest revenue $\max_{i} r_{i1}$ is optimal.
Proposition 2 (p. 14). If $S^*$ is optimal and $S^*_i \ne \emptyset$ , then $R_i(S^*_i) \ge Z^*$ .
Lemma 3 (p. 14). If $Z = \Pi(S)$ , $R_i(S_i) \ge Z$ and some $j \in S_i$ has $r_{ij} < \gamma_i Z + (1-\gamma_i) R_i(S_i)$ , removing $j$ strictly increases the expected revenue.
$g(\alpha) \le \gamma$ (p. 15). For $0 < \gamma \le 1$ and $0 < \alpha < 1$ : $(1 - \alpha^{\gamma})/(\alpha^{\gamma-1} - \alpha^{\gamma}) \le \gamma$ .
Revenue threshold (p. 15). Every $j \in S^*_i$ of an optimal $S^*$ has $r_{ij} \ge \gamma_i Z^* + (1-\gamma_i) R_i(S^*_i)$ .
$h(\alpha) \ge \gamma$ (p. 16). For $0 < \gamma \le 1$ and $0 < \alpha < 1$ : $(1 - \alpha^{\gamma})/(1 - \alpha) \ge \gamma$ .
Exchange step (p. 15). If $S^*$ is optimal, $j \in S^*_i$ , $k \notin S^*_i$ and $k < j$ , then adding $k$ to $S^*_i$ keeps the assortment optimal.

A companion item (not a milestone) states the algorithmic consequence at the end of §3: solving the linear program (4) over the candidates $\{N_{ij} : j \in N_+\}$ and choosing in each nest a maximizer of problem (5) gives an optimal solution of (2).

Significance

Theorem 4 reduces problem (2), a search over $2^{mn}$ assortments, to $(n+1)^m$ nested-by-revenue combinations, and the paper then finds the best one with a linear program with $1 + m$ variables and $1 + m(1+n)$ constraints. It marks the exact boundary of the classical multinomial logit structure inside the nested logit model: the paper's §4 shows that a single nest with $\gamma_i > 1$ already breaks it, and that the general problem is NP-hard. The structural statement is also the base case for the approximation guarantees of §§5–6, which compare against nested-by-revenue assortments.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. A formal proof would supply a verified reduction from a combinatorial revenue maximization over the nested logit model to a polynomial-size search, with every boundary case (empty nests, $v_0 = 0$ , ties in revenues) handled explicitly.

Difficulty

The obvious argument copies the multinomial logit proof: take an optimal assortment and swap a low-revenue product for a missing higher-revenue one. Under the nested logit model this exchange changes the nest's attraction $V_i(S_i)^{\gamma_i}$ non-linearly, so the revenue of the modified assortment is not an affine function of the change, and a simple swap can lower the expected revenue. The argument must instead control how adding or removing one product moves the nest weight relative to the nest revenue, and this is exactly where $\gamma_i \le 1$ enters, through two scalar inequalities in the ratio $\alpha$ of nest weights. With $\gamma_i > 1$ these inequalities fail and so does the theorem.

A second subtlety is ties: several optimal assortments may exist, and only some of them are nested by revenue. The statement asserts existence, not that every optimum has this form.

Formalization scope

All statements live in the namespace NestedLogitVariants.Competitive and share one definition file. Nests form a finite type ι with decidable equality; products are Fin n, indexed $0, \dots, n-1$ , so $N_{ij}$ is nbr n j $= \{k : k < j\}$ with $j \le n$ , and $j = 0$ gives $\emptyset$ . Powers are Real.rpow, and $x / 0 = 0$ , which gives $R_i(\emptyset) = 0$ . Optimality of an assortment means its revenue is at least that of every assortment.

Standing assumptions carried as hypotheses: $v_0 \ge 0$ , $v_{i0} \ge 0$ , revenues ordered within each nest, and §3's $\gamma_i \le 1$ and $v_{i0} = 0$ . Three pins are disclosed: $v_{ij} > 0$ (the paper allows zero-weight padding products, under which Proposition 2 fails), $r_{ij} \ge 0$ , and $\gamma_i > 0$ (the paper's $\gamma_i \ge 0$ ; its convention $V_i(\emptyset)^{\gamma_i} = 0$ fails at $\gamma_i = 0$ ). The section's "without loss of generality $v_0 > 0$ " is a hypothesis of Proposition 2, Lemma 3, the threshold, the exchange step and the LP item; the goal itself only assumes $v_0 \ge 0$ , and the case $v_0 = 0$ is milestone 1. The two scalar inequalities are stated as inequalities, not as monotonicity claims.

The goal is not trivialized by any hypothesis: it assumes none of the milestones, and stating "some nested-by-revenue assortment exists" (always true) or "every optimal assortment is nested by revenue" (false under ties) would be a different theorem.

Needed infrastructure is light: finite sums, real powers, and concavity of $x \mapsto x^{\gamma}$ for $\gamma \le 1$ . The scalar lemmas are reusable for other nested logit results. Proofs of any milestone are welcome independently.

Selected references

J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 250–273, 2014. https://doi.org/10.1287/opre.2014.1256 (cited from the authors' revised manuscript of June 18, 2013)
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
D. McFadden, Modelling the choice of residential location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 75–96, 1978.

9 thms3 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

The Big Data Newsvendor: Practical Insights from Machine Learning: The L2-Regularized Feature-Based Newsvendor Rule Generalizes with a Bound Free of the Number of FeaturesResearch Paper

Motivation

The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders $q$ units before demand $D$ is observed, and pays a unit backordering cost $b$ for each unit of unmet demand and a unit holding cost $h$ for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.

Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features $p$ is comparable to the sample size $n$ ("big data"), a bound that grows with $p$ says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on $p$ .

This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.

Setting

Cost. For an order $q$ and a demand $d$ , the newsvendor cost is

C(q;d)=b\,(d-q)^+ + h\,(q-d)^+ ,\qquad b,h>0 .

Write $b\vee h=\max(b,h)$ .

Data. A data point is a pair $z=(x,d)$ of a feature vector $x\in\mathbb R^p$ and a demand $d\in\mathbb R$ . Features lie in a domain $\mathcal X$ inside the ball $\|x\|_2^2\le X_{\max}^2$ , and demands lie in $\mathcal D=[0,\bar D]$ . A sample $S_n=\{(x_i,d_i)\}_{i=1}^n$ consists of $n$ independent draws from an unknown probability distribution $\mu$ concentrated on $\mathcal X\times\mathcal D$ .

Rules and risks. A vector $q\in\mathbb R^p$ defines the linear decision rule $q(x)=q^\top x$ . Its true risk and empirical risk are

R_{true}(q)=\mathbb E_{(x,d)\sim\mu}\bigl[C(q^\top x;d)\bigr],\qquad \hat R(q;S_n)=\frac1n\sum_{i=1}^n C(q^\top x_i;d_i).

The regularized algorithm (NV-reg). For a parameter $\lambda>0$ , the rule $\hat q=\hat q(S_n)$ minimizes

\hat R(q;S_n)+\lambda\|q\|_2^2\qquad\text{over } q\in\mathbb R^p .

The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from $\mathcal X\times\mathcal D$ are assumed to map $\mathcal X$ into $\mathcal D$ (the paper's $\mathcal Q\subset\mathcal D^{\mathcal X}$ ): the learned order quantity is never negative and never exceeds the demand cap.

Uniform stability. An algorithm is uniformly stable with parameter $\alpha_n$ if removing one observation from any sample changes the loss of its output at any test point by at most $\alpha_n$ (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).

Formalization targets

Goal: Theorem 2 (p. 9)

For every $\delta\in(0,1)$ and $n\ge1$ , with probability at least $1-\delta$ over $S_n$ ,

|R_{true}(\hat q)-\hat R(\hat q;S_n)|\le\frac{(b\vee h)^2X_{\max}^2}{n\lambda}+\Bigl(\frac{2(b\vee h)^2X_{\max}^2}{\lambda}+(b\vee h)\bar D\Bigr)\sqrt{\frac{\ln(2/\delta)}{2n}} .

The dimension $p$ appears nowhere in the bound.

Milestones, in the order of the proof (p. 32)

Lemma 5 (p. 28). For $q,d\in[0,\bar D]$ , $|C(q;d)|\le(b\vee h)\bar D$ , and the bound is attained.
Display (31) (p. 31). $C$ is convex in its first argument and $(b\vee h)$ -Lipschitz in it, i.e. $(b\vee h)$ -admissible in the sense of Definition 2.
Theorem 5 (p. 31), Bousquet and Elisseeff's Theorem 22: regularization in a reproducing kernel Hilbert space with a $\sigma$ -admissible loss and kernel bound $\kappa^2$ has uniform stability $\sigma^2\kappa^2/(2\lambda n)$ . This is an existing platform statement, referenced rather than restated.
Theorem 4 (p. 30). (NV-reg) is uniformly stable with parameter $\alpha_n^r=(b\vee h)^2X_{\max}^2/(2n\lambda)$ .
Theorem 6 (p. 31). Any algorithm with uniform stability $\alpha_n$ and loss in $[0,M]$ satisfies, with probability at least $1-\delta$ ,

|R_{true}(A,S_n)-\hat R(A,S_n)|\le2\alpha_n+(4n\alpha_n+M)\sqrt{\frac{\ln(2/\delta)}{2n}} .

Significance

The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate $O(1/\sqrt n)$ with constants that depend on the costs, the demand cap, the feature radius and $\lambda$ , but not on the number of features. It gives a theoretical basis for regularizing when $p/n$ is not small, and it indicates how to scale $\lambda$ with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in $p$ .

Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.

Difficulty

The bound is not a uniform-convergence argument: the class of linear rules on $\mathbb R^p$ has complexity growing with $p$ , so any bound that holds simultaneously for all rules in the class depends on $p$ . The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.

The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on $n-1$ points it carries the weight $1/(n-1)$ , and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight $1/n$ , which is the form of Theorem 5.

Formalization scope

Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost $h$ and underage cost $b$ ; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its $1/n$ -weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is $\lambda\|q\|_2^2$ (the display prints both $\lambda\|q\|_2^2$ and $\lambda\|q\|_2$ ; the text calls the problem a quadratic program). "With probability at least $1-\delta$ " is stated as: the event on which the gap exceeds the bound has measure at most $\delta$ under the product measure $\mu^n$ .

Standing assumptions and pinned hypotheses.

$b,h,\lambda>0$ , $X_{\max},\bar D\ge0$ , $n\ge1$ , $\delta\in(0,1)$ .
$\mu$ is a probability measure giving full mass to $\mathcal X\times[0,\bar D]$ , with $\|x\|_2^2\le X_{\max}^2$ on $\mathcal X$ (§3, p. 9; the page writes the ball as $\|x\|_2^2\le X_{\max}$ , while Theorem 2's " $X_{\max}^2$ as the largest possible value of $\|x\|_2^2$ " and Theorem 5's note fix the reading).
The algorithm is any map $S_n\mapsto\hat q(S_n)$ whose value minimizes the (NV-reg) objective, measurable in $S_n$ (Appendix B: "all functions are measurable").
The range assumption of Appendix B: for samples from $\mathcal X\times\mathcal D$ , $\hat q^\top x\in[0,\bar D]$ for $x\in\mathcal X$ .
The last constant is $(b\vee h)\bar D$ , the loss bound $M$ from Lemma 5 that the proof feeds into Theorem 6; display (6) prints $\bar D$ there.
The convention that all sets are countable, and the intercept convention $x^1=1$ , are not imposed.

Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in $\mathcal X$ and over samples drawn from $\mathcal X\times\mathcal D$ ; stated over the whole ball $\|x\|_2\le X_{\max}$ , it would force $\hat q=0$ (both $\hat q^\top x$ and $\hat q^\top(-x)$ would lie in $[0,\bar D]$ ) and the goal would be nearly empty.

What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on $\mathbb R^p$ ; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.

Selected references

C. Rudin and G.-Y. Vahn, The Big Data Newsvendor: Practical Insights from Machine Learning, MIT Sloan School Working Paper 5036-13, version of February 6, 2014 (MIT DSpace). The version formalized here.
G.-Y. Ban and C. Rudin, The Big Data Newsvendor: Practical Insights from Machine Learning, Operations Research 67(1):90–108, 2019. https://doi.org/10.1287/opre.2018.1757
O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2:499–526, 2002. https://jmlr.org/papers/v2/bousquet02a.html
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, London Math. Soc. Lecture Note Series 141, 148–188, 1989. https://doi.org/10.1017/CBO9781107359949.008

13 thms3 active usersReviewed

Completed

Convex Optimization Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 3: The Conditional Logit Likelihood Has a Maximum Exactly When No Direction Makes Every Observed Choice Weakly BestResearch Paper

Motivation

The conditional logit model is the workhorse of discrete choice analysis in transportation, marketing, labour and industrial organization. McFadden's 1974 chapter derived it from a theory of population choice behaviour and showed how to estimate it by maximum likelihood; this line of work was recognized by his 2000 Nobel Prize in Economic Sciences, awarded for theory and methods of discrete choice analysis. Every applied logit estimation rests on a basic question: does the maximum likelihood estimate exist for the sample at hand? In small samples it may not. When one alternative is always chosen whenever it is available, the likelihood keeps increasing as a parameter tends to infinity, and numerical optimizers report diverging coefficients. This failure is known in the binary case as complete or quasi-complete separation. McFadden's Lemma 3 gives the exact condition, for the multinomial conditional logit model with general alternative sets, under which a maximizer exists.

Timeline. Berkson (1951, 1955) popularized binomial logit; multinomial versions were developed by Gurland (1960), Bloch (1967), Rassam (1971), McFadden (1968) and Theil (1969, 1970). McFadden (1974) stated the existence criterion for the conditional logit likelihood (Lemma 3) together with a quadratic-programming test for it (Lemma 4). Albert and Anderson (1984) later classified separation patterns for binary and multinomial logistic regression, and Haberman (1974) treated existence for log-linear models.

Setting

A choice experiment has $N \ge 1$ trials. Trial $n$ offers an alternative set of $J_n$ alternatives, indexed $i = 1,\dots,J_n$ , each described by an attribute vector $z_{in} \in \mathbb{R}^K$ (the values of $K$ specified functions of the individual's and the alternative's characteristics). Trial $n$ is repeated $R_n \ge 1$ times, and alternative $i$ is chosen $S_{in}$ times, so $R_n = \sum_{j} S_{jn}$ .

For a parameter $\theta \in \mathbb{R}^K$ , with $z_{in}\theta$ the inner product, the selection probabilities are

P_{in}(\theta) = \frac{e^{z_{in}\theta}}{\sum_{j=1}^{J_n} e^{z_{jn}\theta}} \qquad (16)

and the log-likelihood of the sample is

L(\theta) = C - \sum_{n=1}^N \sum_{i=1}^{J_n} S_{in} \log \sum_{j=1}^{J_n} e^{(z_{jn} - z_{in})\theta}, \qquad C = \sum_{n=1}^N \Big[\log R_n! - \sum_{j=1}^{J_n}\log S_{jn}!\Big]. \qquad (18)

Write $\bar z_n(\theta) = \sum_i z_{in}P_{in}(\theta)$ for the probability-weighted mean attribute vector of trial $n$ .

Axiom 5 (Full Rank). The $\big(\sum_n J_n\big)\times K$ matrix with rows $z_{in} - \bar z_n$ has rank $K$ .

Axiom 6. There is no nonzero $\gamma \in \mathbb{R}^K$ with $S_{in}(z_{jn} - z_{in})\gamma \le 0$ for all $i, j = 1,\dots,J_n$ and $n = 1,\dots,N$ . Equivalently, no nonzero direction makes every observed choice weakly best in its alternative set.

Formalization targets

Goal: Lemma 3

Under Axiom 5,

\big(\exists\, \hat\theta \in \mathbb{R}^K,\ \forall \theta,\ L(\theta) \le L(\hat\theta)\big) \iff \text{Axiom 6}.

Milestones

Equation (19): the gradient $\partial L/\partial\theta = \sum_n \sum_j (S_{jn} - R_nP_{jn}) z_{jn}$ .
Equation (20): the Hessian $\partial^2L/\partial\theta\,\partial\theta' = -\sum_n R_n \sum_j (z_{jn} - \bar z_n)'P_{jn}(z_{jn} - \bar z_n)$ .
$L$ is concave, and every critical point is a global maximizer.
A Hessian that is nonsingular everywhere makes $L$ strictly concave with at most one maximizer.
Axiom 5 holds at $\theta$ if and only if the Hessian at $\theta$ is negative definite.
Necessity: under Axiom 5, a maximizer forces Axiom 6.
Equation (21): under Axiom 6, $b(\gamma) = \max_n \max_{i,j} S_{in}(z_{jn}-z_{in})\gamma$ has a positive lower bound $b^*$ on the unit sphere.
The bound $L(\theta) - C \le -b^*|\theta|$ for all $\theta$ .
Sufficiency: Axiom 6 gives a maximizer.

Significance

Lemma 3 tells the practitioner when the conditional logit maximum likelihood estimate exists, before any numerical optimization is attempted. It is a linear-inequality condition on the data alone, so it can be checked by linear or quadratic programming (Lemma 4 of the same paper). The existence of the estimator is also the first step of McFadden's asymptotic theory: Lemma 5 shows that Axiom 6 holds with probability tending to one, and Lemma 6, consistency and asymptotic normality, concerns the estimator whose existence Lemma 3 characterizes. The concavity and Hessian formulas (19)–(20) are the basis of the Newton–Raphson computation of the estimator and of its asymptotic covariance matrix.

The result has been proved since 1974 and is classical. To our knowledge it has no machine-checked proof; Mathlib has no statement about the existence of logit or softmax-regression maximum likelihood estimates. Formalizing it produces a verified existence criterion for the multinomial logit likelihood, verified gradient and Hessian formulas for log-sum-exp likelihoods with repeated observations, and a verified link between full column rank and strict concavity.

Difficulty

The likelihood is concave, and concave functions on $\mathbb{R}^K$ need not attain their supremum. Concavity alone therefore gives nothing, and existence must come from a growth condition. The obvious approach, "the likelihood is bounded above by $C$ , hence attains its maximum", fails: $L$ is bounded but can approach its supremum only at infinity, which is exactly the separation case. Sufficiency needs a quantitative rate at which $L$ decreases, uniform over all directions; a direction-by-direction argument does not suffice. Necessity requires strict concavity, which is where Axiom 5 and the requirement that every trial be observed enter. A trial with $R_n = 0$ can supply the rank of Axiom 5 while contributing nothing to $L$ , so with such a trial necessity fails. The calculus part, (19)–(20), involves differentiating sums of log-sum-exp terms over dependent index types and identifying the result with a weighted covariance operator.

Formalization scope

Representation. $\mathbb{R}^K$ is EuclideanSpace ℝ (Fin K), so $|\theta| = (\theta'\theta)^{1/2}$ is the Euclidean norm and $z\theta$ is the inner product ⟪z, θ⟫. Trials are Fin N, alternatives of trial $n$ are Fin (J n), and the counts $S_{in}$ are natural numbers.
Data structure. The structure Data K bundles $N$ , $J$ , $z$ , $S$ and the standing assumptions $N \ge 1$ and $R_n = \sum_i S_{in} \ge 1$ for every trial; these make the trial and alternative index sets nonempty.
Axioms 1–4 are built in. The model is the logit form (16) with $v$ linear in $\theta$ (Axiom 4), so "Suppose Axioms 1–5 hold" becomes "Data plus Axiom 5".
Axiom 5 is read at every $\theta$ . The row space of the matrix does not depend on $\theta$ .
Hessian. The Hessian is the Fréchet derivative of the gradient vector field (19), as a continuous linear map.
The maximizer is global over all of $\mathbb{R}^K$ . Neither a local maximizer nor " $L(\hat\theta) \ge L(0)$ " is acceptable as the goal; that would make it trivial.
Infrastructure. Gradients and Hessians of log-sum-exp with dependent finite index types; positive definiteness from full column rank; attainment of the maximum of a coercive continuous function on a finite-dimensional space. The calculus lemmas are reusable for any multinomial logit or softmax likelihood. Missions 4 and 5 of this series reuse the same model. Contributions of general log-sum-exp lemmas, independent of this mission's definitions, are welcome.

Selected references

D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
A. Albert and J. A. Anderson, On the existence of maximum likelihood estimates in logistic regression models, Biometrika 71(1), 1984, pp. 1–10. https://doi.org/10.1093/biomet/71.1.1
S. J. Haberman, The Analysis of Frequency Data, University of Chicago Press, 1974.
J. Berkson, Maximum likelihood and minimum χ² estimates of the logistic function, Journal of the American Statistical Association 50, 1955, pp. 130–162. https://doi.org/10.1080/01621459.1955.10501255

12 thms3 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Reversibility and Stochastic Networks IX: Partial Balance — Equivalent Characterizations via Truncation, Rate Changes and Time ReversalTextbook

Why partial balance

Equilibrium distributions of Markov models of networks are rarely computed by solving the full equilibrium equations directly. In the classical product-form results (migration processes, Jackson and Kelly networks, loss networks, clustering processes) the equilibrium distribution satisfies a stronger, local family of equations, and that is what makes it computable. The strongest such family is detailed balance, which characterizes reversibility. Many models that are not reversible still satisfy an intermediate family, partial balance: the probability flux balances not pair by pair but across a chosen set of transitions. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) uses partial balance throughout: quasi-reversibility in Chapter 3 is a form of it, and the models that display it tend to be insensitive, meaning their equilibrium distribution does not change when exponential holding times are replaced by general ones with the same mean.

Section 9.4 of the book collects what partial balance means in a single statement. Theorem 9.5 summarizes Exercises 1.6.2–1.6.4 and 1.7.7–1.7.8 and gives five operational characterizations of partial balance. Corollaries 9.6–9.8 translate them into the language of spatial processes, and Theorem 9.9 turns partial balance of a coarse description into a product-form equilibrium for a finer one. This last step is the mechanism behind insensitivity.

Setting

A Markov process on a state space $\mathcal S$ has transition rates $q(j,k)\ge0$ for $j\ne k$ , with $q(j,j)=0$ . It is irreducible: every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers $\pi(j)$ summing to one that satisfies the equilibrium equations

\pi(j)\sum_{k\in\mathcal S}q(j,k)=\sum_{k\in\mathcal S}\pi(k)q(k,j),\qquad j\in\mathcal S.

For an irreducible process on a finite state space it exists and is unique.

Given a set $\mathcal A\subseteq\mathcal S$ , $\pi$ satisfies partial balance with respect to $\mathcal A$ if

\pi(j)\sum_{k\in\mathcal A}q(j,k)=\sum_{k\in\mathcal A}\pi(k)q(k,j),\qquad j\in\mathcal A.

Truncating the process to $\mathcal A$ deletes every transition out of $\mathcal A$ , and the result is required to be irreducible within $\mathcal A$ . The time-reversed process of a process with equilibrium distribution $\pi$ has rates $\pi(k)q(k,j)/\pi(j)$ .

A spatial process has $J$ sites, the vertices of a graph $G$ . Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$ , and the state space is $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$ . Write $T_j^m\mathbf n$ for the state $\mathbf n$ with the attribute of site $j$ changed to $m$ . The process must satisfy three conditions: only one site changes at a time; the rate $q(\mathbf n,T_j^m\mathbf n)$ depends on the other sites only through the neighbours of $j$ ; and any $T_j^m\mathbf n$ can be reached from $\mathbf n$ without changing the other sites. The conditional distribution of site $j$ given the rest is $P(n_j\mid\mathbf n_{G-j})=\pi(\mathbf n)/\sum_m\pi(T_j^m\mathbf n)$ . A Markov field is a positive distribution whose conditional distributions depend only on the neighbours of $j$ .

Formalization targets

Goal: Theorem 9.5

For an irreducible process on a finite $\mathcal S$ with equilibrium distribution $\pi$ , a nonempty $\mathcal A$ within which the truncated process is irreducible, and a constant $c>0$ , $c\ne1$ , the following are equivalent:

partial balance with respect to $\mathcal A$ ;
the equilibrium distribution of the truncated process is $\pi(j)/\sum_{k\in\mathcal A}\pi(k)$ ;
multiplying the rates $q(j,k)$ , $j,k\in\mathcal A$ , by $c$ leaves the equilibrium distribution unchanged;
multiplying the rates $q(j,k)$ , $j\in\mathcal A$ , $k\notin\mathcal A$ , by $c$ changes the equilibrium distribution to

B\pi(j)\ (j\in\mathcal A),\qquad Bc\pi(j)\ (j\notin\mathcal A),\qquad B^{-1}=\sum_{j\in\mathcal A}\pi(j)+c\sum_{j\notin\mathcal A}\pi(j);

time reversal and truncation to $\mathcal A$ commute.

When $\mathcal S-\mathcal A$ is nonempty, these are also equivalent to:

the chain observed just before each exit from $\mathcal A$ and the chain observed just after each entry into $\mathcal A$ have the same equilibrium distribution.

Milestones

Corollary 9.6: the equivalences for the sets on which all sites but $j$ are frozen, i.e. partial balance (9.26) at a site.
Corollary 9.7: on a state space with at least two states, partial balance at every site makes $\pi$ a Markov field, with $0<\pi(\mathbf n)<1$ as in the book's definition.
Corollary 9.8: the equivalences for the set on which site $j$ is frozen at one attribute (9.27).
Theorem 9.9: if a reduced description $\mathbf n=f(\mathbf x)$ has a distribution $\pi(\mathbf n)$ in partial balance for the rates (9.31), then the finer process has equilibrium distribution $\pi(\mathbf x)=\pi(\mathbf n)\prod_jP_j(x_j\mid n_j)$ .

What the results give

Theorem 9.5 makes partial balance testable by operations on the process itself: truncation, speeding up or slowing down transitions, and time reversal. The book points to close relationships between statement (iv) and the product form of Section 2.3, and between statement (ii) and part (iii) of Theorem 3.12. Corollary 9.6 (iv) explains why the reversed migration process has such a simple form. Corollary 9.7 strengthens Theorem 9.3 by replacing reversibility with partial balance at each site. Theorem 9.9 is the step from partial balance to insensitivity: it is what the book uses to show that a spatial process keeps its equilibrium distribution when the lifetimes of attributes are mixtures of gamma distributions.

All of these results were proved in 1979. None has a machine-checked proof. The platform has the reversible special case of statement (ii) (KellyStochasticNetworks.truncated_reversible) and the rate-level objects for time reversal and truncation, which this mission reuses. Formalizing Theorem 9.5 also produces a reusable account of embedded exit and entry chains of a finite Markov process.

Difficulty

Most of the equivalences (i)–(v) are short manipulations of the equilibrium equations, but each direction from a property of an altered process back to partial balance needs uniqueness of equilibrium distributions for irreducible finite processes, and (v) ⇒ (i) also needs their existence. Mathlib has neither in the form needed here. Statement (vi) is a different kind of claim. The equilibrium distribution of the exit chain is proportional to the exit flux $\pi(j)\sum_{k\notin\mathcal A}q(j,k)$ , and that of the entry chain to the entry flux. Proving this requires the hitting distributions and the Green's function of the jump chain killed on leaving a set, and the convergence of the series that define them. Corollary 9.8 (v) inherits that work. Theorem 9.9 requires uniqueness for the reduced frozen processes and careful bookkeeping of the fibres $\{x_j:f_j(x_j)=n_j\}$ .

Formalization scope

State spaces are finite types, and every sum is an unconditional sum over a finite type. Because the state space is finite, the book's extra condition for (vi), a finite flux out of $\mathcal A$ , holds automatically. Rates are real functions with $q(j,j)=0$ built into the hypotheses; the reduced rates of (9.31) also have zero self-rates. "The equilibrium distribution of a process is $X$ " means: $X$ is positive, sums to one, satisfies the equilibrium equations, and every distribution with these properties equals $X$ . The book's " $c\ne0$ or $1$ " is read as $c>0$ , $c\ne1$ , so that altered rates remain rates. Truncation to $\mathcal A$ is the published truncatedRates, a process on the subtype $\mathcal A$ , and the reversed rates are the published reversedRates. The exit and entry chains are defined from the jump chain through series of restricted matrix powers. Spatial processes live on $\prod_j\mathcal N_j$ with $T_j^m$ given by Function.update. In Theorem 9.9 the graph is complete, as the book assumes from p. 202 on.

The equilibrium distribution of the truncated process must be the unique positive normalized solution of the truncated equilibrium equations. It must not be defined as the conditional distribution, which would make (ii) a tautology. For the same reason (iii) and (iv) are stated through the equilibrium equations of the altered rates, not by assumption.

Theorem 9.10 (p. 207) is not a target. Its hypothesis, that a nominal lifetime "can have any distribution with unit mean", is not defined on the page, and the point-process and lifetime description it needs lies outside this rate-level development.

Contributions are welcome at every level: uniqueness and existence of equilibrium distributions for irreducible finite rate matrices (reusable across the series), convergence of the killed Green's function, and proofs of the corollaries from the goal.

Selected references

F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979; reissued Cambridge University Press, 2011. https://doi.org/10.1017/CBO9781139171724 (§9.4, pp. 200–208; §1.6, pp. 25–27)
F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

11 thms3 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 2: Random Utility Maximizers Choose by Logit Exactly When Taste Shocks Are Extreme-Value DistributedResearch Paper

Motivation

The conditional logit model assigns to an alternative $i$ in a finite choice set the probability $e^{V_i}/\sum_j e^{V_j}$ , where $V_j$ is a "representative utility" built from observed attributes of the alternative and the decision maker. It is the workhorse of discrete choice econometrics, transportation demand forecasting, marketing and revenue management, where it underlies multinomial logit assortment and pricing models. Its appeal for applied work is computational; its appeal for economics is that it can be read as the aggregate behaviour of a population of utility maximizers. This mission formalizes the result that makes that reading exact: Lemmas 1 and 2 of D. McFadden, Conditional logit analysis of qualitative choice behavior (1974), which show that, under a mild regularity condition, logit choice probabilities arise from random utility maximization exactly when the idiosyncratic taste shocks follow the extreme value (Gumbel) distribution.

Timeline:

1959. J. Marschak gives a nonconstructive proof that i.i.d. extreme value shocks yield logit probabilities; R. D. Luce's choice axiom appears the same year.
1965. Luce and Suppes publish the constructive argument, attributed to E. Holman and A. Marley, that is reproduced as the proof of Lemma 1.
1974. McFadden proves the converse (Lemma 2): if i.i.d. shocks with a translation complete distribution produce logit probabilities, the distribution is extreme value.
Later. The random utility characterization was extended to correlated shocks (generalized extreme value models, McFadden 1978), which are not part of this mission.

Setting

An individual faces $J \ge 1$ alternatives with representative utilities $V_1, \dots, V_J \in \mathbb{R}$ . The utility of alternative $j$ is $U_j = V_j + \varepsilon_j$ , where the taste shocks $\varepsilon_1, \dots, \varepsilon_J$ are independent and identically distributed with a common law $\mu$ on $\mathbb{R}$ and distribution function $G(t) = \mu((-\infty, t])$ . The individual chooses the alternative of highest utility, so the selection probability of $i$ is (Equation (2) of the paper)

P_i(V) = \Pr\big[\varepsilon_j - \varepsilon_i < V_i - V_j \ \text{ for all } j \ne i\big],

computed under the product law of the shocks. The logit formula (Equation (12)) is $L_i(V) = e^{V_i}/\sum_{j=1}^J e^{V_j}$ . The extreme value law (Equation (13)) is $G(\varepsilon) = e^{-e^{-\varepsilon}}$ .

A law $\mu$ is translation complete if for every function $h$ of bounded total variation on $\mathbb{R}$ with $h(\pm\infty) = 0$ , the condition $\int h(e + a)\, d\mu(e) = 0$ for every real $a$ forces $h = 0$ outside a Lebesgue-null set. Laws whose characteristic function never vanishes, the extreme value law among them, are translation complete (footnote 5 of the paper).

In Lean the law is μ : Measure ℝ with [IsProbabilityMeasure μ], $G$ is ProbabilityTheory.cdf μ, the selection probability is selProb μ V i for V : Fin J → ℝ, and the logit formula is logitProb V i.

Formalization targets

Goal: the characterization

Fix a universe $X$ of alternatives with a representative utility map $u:X\to\mathbb R$ onto the real line. For a translation complete law $\mu$ normalized by $G(0) = e^{-1}$ ,

\Big(\text{for every finite }B\subseteq X,\ i\in B:\ P_i(B) = \frac{e^{u(i)}}{\sum_{j\in B} e^{u(j)}}\Big) \iff \Big(\forall \varepsilon \in \mathbb{R}:\ G(\varepsilon) = e^{-e^{-\varepsilon}}\Big).

The normalization only fixes the location of the shocks: without it the conclusion is the one-parameter family of Lemma 2 below.

Milestones

Equation (3) for i.i.d. shocks without atoms: $P_i(V) = \int \prod_{j \ne i} G(\varepsilon + V_i - V_j)\, dG(\varepsilon)$ .
The integrand of Lemma 1's proof: under (13), the density times the other distribution functions equals $e^{-\varepsilon} \exp\big(-e^{-\varepsilon} \sum_j e^{V_j - V_i}\big)$ .
Lemma 1: extreme value shocks give $P_i(V) = L_i(V)$ for every $J$ and $V$ .
The functional equation of Lemma 2's proof: $G(v - \log K) = G(v)^K$ for every positive integer $K$ and real $v$ .
Values at logarithms of rationals: with $\alpha = -\log G(0)$ , $\alpha > 0$ and $G(\log(K/L)) = e^{-\alpha L / K}$ for positive integers $K, L$ .
Lemma 2: $G(\varepsilon) = e^{-\alpha e^{-\varepsilon}}$ for some $\alpha > 0$ , and $G(0) = e^{-1}$ gives (13).

Significance

The result separates two readings of the logit formula. Lemma 1 shows that it is consistent with utility maximization; Lemma 2 shows that, within the class of i.i.d. additive random utility models with translation complete shocks, the extreme value law is the only one consistent with it. Consequences drawn from the random utility reading, such as the log-sum formula for expected maximum utility used in welfare analysis, therefore apply to logit models without further distributional assumptions inside that class. The same reading supports the interpretation of multinomial logit demand in assortment optimization and revenue management.

Both lemmas are proved in the paper and in later textbooks; neither is open. As far as a search of the Prove2Me catalog shows, neither has a machine-checked proof. The mission provides Lean statements of the random utility model with i.i.d. shocks, of translation completeness and of the extreme value law that later discrete choice formalizations can reuse.

Difficulty

Lemma 1 is a computation with the extreme value density; its formal cost lies in passing from the product-measure probability (2) to the iterated integral (3) and evaluating an improper integral. Lemma 2 is harder. The natural first idea is to differentiate the logit identity in the utilities and solve a differential equation for $G$ ; this requires a density, which Lemma 2 does not assume. Without a density, the only handle on $G$ is the logit identity itself, an equality of integrals against $dG$ that holds for every utility vector; turning such integral identities into pointwise information about $G$ is where the hypothesis of translation completeness enters, and it yields statements only outside a Lebesgue-null set, so one-sided continuity of distribution functions is needed to recover identities at every point. A second subtlety is that the paper's (14) is written with $G$ while the event (2) is strict, so with a general law the integrals involve left limits of $G$ .

Formalization scope

Alternatives are indexed by Fin J; the model is indexed by the utility vector, so the individual attributes $s$ and alternative attributes $x_j$ enter only through $V$ . The shocks have joint law Measure.pi (fun _ => μ), which is what "independently identically distributed" means; a general joint law is not allowed. The event in (2) uses strict inequalities, and the selection probability is defined for every law, with no density. Translation completeness quantifies over BoundedVariationOn h Set.univ with limits $0$ at both ends; such $h$ are bounded and measurable, so the integrals are genuine, and "measure zero" is Lebesgue measure.

Lemma 2's hypothesis is stated on every finite subset of the paper's alternative universe, with a surjective utility map. Distinct alternatives may have the same utility. The printed proof uses $K$ equal-utility alternatives, which surjectivity alone need not supply; proving the stated theorem requires an additional continuity argument. A trivializing formalization is ruled out: the selection probability is a genuine product-measure probability, and the hypotheses of the goal are met by the extreme value law, which is translation complete with $G(0) = e^{-1}$ .

A complete development needs: Fubini for Measure.pi over Fin J split at one coordinate; the Gumbel density and the improper integral $\int e^{-\varepsilon} e^{-c e^{-\varepsilon}} d\varepsilon = 1/c$ ; the facts that bounded-variation functions are bounded and measurable and that distribution functions are right-continuous with left limits. The integral representation (milestone 1) and the Gumbel computations are reusable in any random utility formalization. Proofs of the milestones, of the footnote-5 fact that the extreme value law is translation complete, and alternative proofs of Lemma 2 are welcome.

Selected references

D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142.
J. Marschak, Binary choice constraints and random utility indicators, in K. Arrow, S. Karlin, P. Suppes (eds.), Mathematical Methods in the Social Sciences, Stanford University Press, 1960 (Stanford Symposium, 1959).
R. D. Luce and P. Suppes, Preference, utility, and subjective probability, in R. D. Luce, R. Bush, E. Galanter (eds.), Handbook of Mathematical Psychology, Vol. III, Wiley, 1965.
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, 1959.
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966, p. 479.
D. McFadden, Modelling the choice of residential location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 1978, pp. 75–96.

8 thms3 active usersReviewed

Completed

Graph Theory Markov Chain Probability+2·Captain: mikedeng1

Reversibility and Stochastic Networks VIII: Markov Fields — A Positive Random Field Is Markov iff It Factorizes over the Simplices of the GraphTextbook

Motivation

Many systems consist of a finite number of sites whose states influence one another only locally: fruit trees in an orchard that are diseased or healthy, power sources that are working or broken, individuals holding one of several views. Chapter 9 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) asks which joint distributions such systems have in equilibrium. Earlier chapters of the book produce product-form distributions in which the components are independent; spatial models instead give a limited dependence, and §9.1 makes that notion precise through Markov fields.

The central characterization, that a positive random field is Markov with respect to a graph exactly when it factorizes over the cliques of that graph, is the theorem of Hammersley and Clifford (1971, unpublished manuscript), with published proofs by Besag (1974), Grimmett (1973) and Preston (1973). It underlies Gibbs random fields in statistical mechanics, spatial statistics, image analysis and graphical models. Kelly's §§9.2–9.3 then use it to identify the equilibrium distributions of interacting-particle Markov processes ("spatial processes"), connecting it to reversibility and partial balance.

Setting

There are $J$ sites, the vertices of a finite graph $G$ ; $\partial j$ is the set of neighbours of site $j$ and $G-j$ the set of sites other than $j$ . Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$ , and a state is $\mathbf n=(n_1,\dots,n_J)$ in $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$ . For a set of sites $H$ , $\mathbf n_H$ is the vector of attributes of the sites in $H$ . The operator $T_j^m$ changes the attribute of site $j$ to $m$ .

A random field is a function $\pi$ on $\mathcal S$ with $\pi(\mathbf n)>0$ for every state and $\sum_{\mathbf n}\pi(\mathbf n)=1$ . The conditional probability that site $j$ has attribute $n_j$ given all other sites is

P(n_j\mid\mathbf n_{G-j}) = \frac{\pi(\mathbf n)}{\sum_{m\in\mathcal N_j}\pi(T_j^m\mathbf n)}. \qquad (9.1)

$\pi$ is a Markov field if $P(n_j\mid\mathbf n_{G-j}) = P(n_j\mid\mathbf n_{\partial j})$ for every $j$ and $\mathbf n$ (9.2): the attribute of a site depends on the rest of the system only through its neighbours. A simplex is a single site or a set of sites any two of which are neighbours; $\mathcal C$ is the set of simplices of $G$ .

A spatial process is a Markov process $\mathbf n(t)$ on $\mathcal S$ with rates $q$ such that (i) only one component changes at a time, (ii) $q(\mathbf n,T_j^m\mathbf n)$ depends on $\mathbf n$ only through $n_j$ and $\mathbf n_{\partial j}$ , and (iii) $T_j^m\mathbf n$ can be reached from $\mathbf n$ by transitions that do not alter $\mathbf n_{G-j}$ . The general spatial process of §9.3 has rates

q(\mathbf n,T_j^m\mathbf n)=\lambda_j(n_j,m)\,\frac{\Phi(\mathbf n)}{\Phi_{G-j}(\mathbf n_{G-j})} \qquad (9.15)

for positive functions $\Phi$ , $\Phi_{G-j}$ .

Formalization targets

Goal: Theorem 9.2 (p. 186)

A random field $\pi$ is a Markov field if and only if

\pi(\mathbf n) = B\prod_{C\in\mathcal C}\phi_C(\mathbf n_C), \qquad \mathbf n\in\mathcal S, \qquad (9.5)

for some constant $B$ and functions $\phi_C$ .

Milestones

Lemma 9.1 (p. 185): the conditional probabilities $P(n_j\mid\mathbf n_{G-j})$ , $j\in G$ , $\mathbf n\in\mathcal S$ , determine the random field uniquely.
Theorem 9.3 (p. 189): the equilibrium distribution of a reversible spatial process is a Markov field.
Theorem 9.4 (p. 193): for the rates (9.15), with $\alpha_j>0$ solving $\alpha_j(n)\sum_m\lambda_j(n,m)=\sum_m\alpha_j(m)\lambda_j(m,n)$ (9.16), the equilibrium distribution is

\pi(\mathbf n) = B\,\frac{\prod_{j=1}^J\alpha_j(n_j)}{\Phi(\mathbf n)}, \qquad (9.17)

and it satisfies the partial balance equations (9.18) site by site.

Significance

Theorem 9.2 turns a statement about conditional laws, which is how local interaction is usually specified, into an explicit parametrization of the joint law by clique potentials. On a lattice with binary attributes it reduces a Markov field to one parameter per site and one per pair of adjacent sites, giving the form $\pi(\mathbf n)=B\alpha^M\beta^R$ (9.9). Theorem 9.3 shows that local, reversible dynamics produce Markov-field equilibria, and Theorem 9.4 gives a family of non-reversible processes, containing the closed migration process of Chapter 2, whose equilibria are still explicit; its partial balance equations are the bridge to §9.4.

All four results are classical and proved in the book. They are not, to our knowledge, machine-checked in this discrete form. The platform has an open statement of Hammersley–Clifford in a different setting, HighDimStat.GraphicalModels.thm11_8_hammersley_clifford (Wainwright, High-Dimensional Statistics, Theorem 11.8): a random vector in $\mathbb R^V$ with a strictly positive Lebesgue density and the global (separation) Markov property. Neither statement implies the other as formalized, so this mission poses Kelly's finite, local version separately. A formal proof here also gives reusable infrastructure: conditional probabilities of a distribution on a finite product space, and factorizations over the cliques of a graph.

Difficulty

The "if" direction is routine. The "only if" direction is where the content lies: the functions $\phi_C$ must be produced from $\pi$ alone, and a product over the cliques of $G$ must reproduce $\pi$ at every state, not only at the states whose nonzero attributes sit on a single clique. The natural first idea, one factor per site read off from the conditional laws, fails as soon as two sites interact. The Markov property must also be brought from its explicit form (9.2), which involves a marginal over the non-neighbours, into a usable statement about $\pi$ itself. Strict positivity is essential: without it the "only if" direction is false (Exercise 9.2.2). For Theorem 9.3, condition (iii) cannot be dropped: Exercise 9.2.2 gives a reversible process satisfying (i) and (ii) whose equilibrium is not a Markov field, so any argument that uses only the local form of the rates fails.

Formalization scope

Sites form an arbitrary finite type V with decidable equality; attributes at site j form a finite type N j, which may differ between sites. States are dependent functions (j : V) → N j, and $T_j^m\mathbf n$ is Function.update n j m. The graph is a Mathlib SimpleGraph V, so $\partial j$ is G.neighborSet j.
A random field is a real function, positive at every state, with finite sum $1$ . $P(n_j\mid\mathbf n_{\partial j})$ is the conditional probability computed from $\pi$ (a ratio of finite sums), so (9.2) is stated literally.
Simplices are the nonempty cliques of the given graph $G$ , including single sites. The factorization ranges over exactly these sets; a product over all subsets of sites, or over the cliques of the complete graph, would make the goal trivially true and is ruled out.
Theorems 9.3 and 9.4 are read at the level of rates: "equilibrium distribution of a reversible process" is a positive distribution summing to one in detailed balance with $q$ (the published KellyStochasticNetworks.DetailedBalance), and "equilibrium distribution" in 9.4 is a positive distribution summing to one satisfying the equilibrium equations (KellyStochasticNetworks.FullBalance), together with its uniqueness under irreducibility. The Markov process itself is not constructed. The state space is always finite, so all sums are finite.
Contributions welcome: proofs of any item, general lemmas on conditional laws over finite product spaces, and a formal account of the general Hammersley–Clifford theorem that both this mission and the Wainwright statement could use.

Selected references

F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 9. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
J. Besag, Spatial interaction and the statistical analysis of lattice systems, J. Roy. Statist. Soc. B 36 (1974), 192–236. https://doi.org/10.1111/j.2517-6161.1974.tb00999.x
G. R. Grimmett, A theorem about random fields, Bull. London Math. Soc. 5 (1973), 81–84. https://doi.org/10.1112/blms/5.1.81
C. J. Preston, Generalized Gibbs states and Markov random fields, Adv. Appl. Probab. 5 (1973), 242–261. https://doi.org/10.2307/1426035
M. J. Wainwright, High-Dimensional Statistics, Cambridge University Press, 2019, Theorem 11.8. https://doi.org/10.1017/9781108627771

8 thms3 active usersReviewed

Completed

Markov Chain Optimization Probability+1·Captain: mikedeng1

Reversibility and Stochastic Networks V: Optimal Capacity Allocation in a Network of QueuesTextbook

Motivation

Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.

The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.

The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.

Setting

Capacity allocation (§4.1). A network has $J \ge 1$ channels. Channel $j$ receives traffic at average rate $a_j > 0$ and is given capacity $\phi_j$ . In equilibrium the number $n_j$ of messages at channel $j$ has the geometric law (4.1),

P(n_j = n) = \Big(1 - \frac{a_j}{\phi_j}\Big)\Big(\frac{a_j}{\phi_j}\Big)^n, \qquad n = 0, 1, 2, \dots,

which requires $\phi_j > a_j$ . Its mean is $a_j/(\phi_j - a_j)$ . Capacity on channel $j$ costs $f_j > 0$ per unit and the total budget is $F$ , giving the cost constraint (4.2)

\sum_j f_j\phi_j = F.

The mean number of customers in the network is

N(\phi) = \sum_j \frac{a_j}{\phi_j - a_j},

and the feasible set is the set of $\phi \in \mathbb{R}^J$ with $\phi_j > a_j$ for every $j$ that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ $= N(\phi) + y(\sum_j f_j\phi_j - F)$ .

Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate $\nu > 0$ at a system of $J$ compartments that is empty at time $0$ . Let $p_j(s)$ be the probability that an individual is in compartment $j$ a time $s$ after its arrival; $p_j(s) \ge 0$ and $\sum_j p_j(s) \le 1$ , since individuals may leave. Let $n_j(t)$ be the number of individuals in compartment $j$ at time $t > 0$ , and

\alpha_j(t) = \int_0^t p_j(u)\,du.

In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and $\alpha_j(t)$ is alpha p j t.

Formalization targets

Goal: Theorem 4.1 (p. 97)

If $J \ge 1$ , $a_j > 0$ , $f_j > 0$ and $F > \sum_k a_k f_k$ , then

\phi^*_j = a_j + \frac{\sqrt{a_j f_j}}{\sum_k \sqrt{a_k f_k}}\cdot\frac{F - \sum_k a_k f_k}{f_j}

is feasible and minimizes $N$ over the feasible set, and every other feasible $\phi$ has $N(\phi) > N(\phi^*)$ .

Milestones toward the goal

The mean of the geometric law (4.1) is $a_j/(\phi_j - a_j)$ (p. 97).
For $y > 0$ the Lagrangian is minimized over $\{\phi_j > a_j\}$ by $\phi_j = a_j + \sqrt{a_j/(y f_j)}$ (proof of Theorem 4.1).
The choice $1/\sqrt y = (F - \sum_k a_k f_k)/\sum_k\sqrt{a_k f_k}$ makes that minimizer equal to $\phi^*$ and feasible for (4.2).

Second result: Theorem 4.2 (pp. 114–115)

The proof's generating-function identity, for $z_j \in [0,1]$ ,

E\big(z_1^{n_1(t)}\cdots z_J^{n_J(t)}\big) = \prod_{j=1}^J \exp\big[-(1 - z_j)\nu\alpha_j(t)\big],

and the theorem itself: $n_1(t), \dots, n_J(t)$ are independent and $n_j(t)$ is Poisson with mean $\nu\alpha_j(t)$ .

Significance

Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity $a_j$ needed to carry its traffic; the remaining budget is shared in proportion to $\sqrt{a_j f_j}$ , not to the traffic $a_j$ . Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.

Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting $t \to \infty$ it recovers the equilibrium Poisson law of §4.5.

Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in $\mathbb{R}^J$ . For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.

Difficulty

For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that $L$ is (strictly) convex on the open region $\phi_j > a_j$ , and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of $\phi^*$ needs $F > \sum_k a_k f_k$ , which the book leaves implicit.

For Theorem 4.2, the steps of the proof that read "conditional on $M$ " have to be carried out with measure-theoretic independence. One step averages a product over $M$ independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of $J$ counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.

Formalization scope

Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.

Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: $J \ge 1$ , $a_j > 0$ , $f_j > 0$ , $F > \sum_k a_k f_k$ . Stability $\phi_j > a_j$ is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of $\phi^*$ , plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that $\phi^*$ satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.

Theorem 4.2. The model is pinned down as in the proof on p. 115:

the number $M$ of arrivals in $(0,t)$ is Poisson with mean $\nu t$ ;
an i.i.d. sequence of (arrival instant, location at time $t$ ) pairs is independent of $M$ , and only its first $M$ entries are used;
each instant is uniform on $(0,t)$ , and an individual arriving at $u$ is in compartment $j$ at time $t$ with probability $p_j(t-u)$ , or has left.

"Individuals move independently" is formalized as this conditional independence. The $p_j$ are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the $J$ counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.

Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for $\mathbb{N}^J$ -valued random vectors.

Selected references

F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979, Chapter 4 (§4.1, pp. 95–97; §4.5, pp. 113–115).
L. Kleinrock, Communication Nets: Stochastic Message Flow and Delay, McGraw-Hill, 1964 (reprinted Dover, 1972).
J. F. C. Kingman, Poisson Processes, Oxford University Press, 1993 (colouring and marking theorems).

8 thms3 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Reversibility and Stochastic Networks III: Open Networks of Queues with General Customer Routes Have Product-Form EquilibriumTextbook

Motivation

Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.

Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served $K$ -server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).

Setting

There are $I$ customer types and $J$ queues. Customers of type $i$ enter the system in a Poisson stream of rate $\nu(i)>0$ and visit the queues $r(i,1),r(i,2),\dots,r(i,S(i))$ in that order before leaving; two successive stages of a route are at different queues.

Queue $j$ holds its $n_j$ customers in positions $1,\dots,n_j$ . Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate $\phi_j(n_j)$ , with $\phi_j(n)>0$ for $n>0$ ; a proportion $\gamma_j(l,n_j)$ goes to the customer in position $l$ . An arriving customer takes position $l$ with probability $\delta_j(l,n_j+1)$ . For each $n\ge1$ , $\gamma_j(\cdot,n)$ and $\delta_j(\cdot,n)$ are probability vectors on $\{1,\dots,n\}$ .

The class of the customer in position $l$ of queue $j$ is $c_j(l)=(t_j(l),s_j(l))$ , his type and the stage of his route. The state of queue $j$ is $\mathbf c_j=(c_j(1),\dots,c_j(n_j))$ and the state of the network is $\mathbf C=(\mathbf c_1,\dots,\mathbf c_J)$ . Its transition rates $q(\mathbf C,\mathbf D)$ , displays (3.1)–(3.6), are the sums of the intensities of all events taking $\mathbf C$ to $\mathbf D$ : a departure from the system (intensity $\phi_j(n_j)\gamma_j(l,n_j)$ ), a move from position $l$ of queue $j$ to position $m$ of the next queue $k$ (intensity $\phi_j(n_j)\gamma_j(l,n_j)\delta_k(m,n_k+1)$ ), and an arrival into position $m$ of the first queue $k$ of a route (intensity $\nu(i)\delta_k(m,n_k+1)$ ).

With $\alpha_j(i,s)=\nu(i)$ if $r(i,s)=j$ and $0$ otherwise, set

a_j=\sum_{i,s}\alpha_j(i,s),\qquad b_j^{-1}=\sum_{n=0}^{\infty}\frac{a_j^n}{\prod_{l=1}^{n}\phi_j(l)},\qquad \pi_j(\mathbf c_j)=b_j\prod_{l=1}^{n_j}\frac{\alpha_j(t_j(l),s_j(l))}{\phi_j(l)}.

Formalization targets

Goal: Theorem 3.1 (p. 61)

If every series defining $b_j^{-1}$ converges, then

\pi(\mathbf C)=\prod_{j=1}^{J}\pi_j(\mathbf c_j)

is positive, sums to $1$ over all network states, and satisfies the equilibrium equations

\pi(\mathbf C)\sum_{\mathbf D}q(\mathbf C,\mathbf D)=\sum_{\mathbf D}\pi(\mathbf D)\,q(\mathbf D,\mathbf C)\quad\text{for every }\mathbf C.

Milestones

Theorem 3.2 (p. 62). The time-reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$ are the rates of the reversed network: routes traversed backwards, $\gamma_j$ and $\delta_j$ interchanged.
Corollary 3.4 (p. 63). Queue $j$ is independent of the rest of the network, is in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$ , holds $n$ customers with probability $b_ja_j^n/\prod_{l=1}^n\phi_j(l)$ (3.7), and a customer in position $l$ is of class $(i,s)$ with probability $\alpha_j(i,s)/a_j$ .
Corollary 3.5 (p. 63). A type- $i$ customer reaching queue $j$ at stage $s$ finds it in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$ .
Lemma 3.13 (p. 89). For a multiclass queue with Poisson arrivals of rate $\nu(c)$ and departure intensities $\nu(c)\phi_c(\mathbf n)$ : reversible $\Leftrightarrow$ quasi-reversible $\Leftrightarrow$ $\Phi(\mathbf n)=\phi_c(\mathbf n)\Phi(\mathbf n-\mathbf e_c)$ for some positive $\Phi$ (3.26).

Significance

Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate $a_j$ , even though the actual arrival stream at queue $j$ is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).

The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.

Difficulty

The obvious first attempt, detailed balance, fails: $\pi(\mathbf C)q(\mathbf C,\mathbf D)$ and $\pi(\mathbf D)q(\mathbf D,\mathbf C)$ differ in general, because a customer's route cannot be run backwards inside the same network ( $q(\mathbf D,\mathbf C)$ is usually $0$ when $q(\mathbf C,\mathbf D)>0$ ). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of $J$ -tuples of lists, reorganized by queue length together with the identity $\sum_{\text{classes at } j}\alpha_j=a_j$ .

Formalization scope

Finite types and queues. Types are Fin I, queues Fin J; the book allows countably many types with $\sum_i\nu(i)<\infty$ . A network state is a function assigning to each queue a list of classes $(i,s)$ with $r(i,s)=j$ ; the state space is countable and all sums over it are tsum/HasSum.
Indexing. Stages and list positions are $0$ -based in Lean; $\gamma_j(l,n)$ and $\delta_j(l,n)$ keep the book's $1$ -based position argument.
Rate level. Equilibrium means: positive, summing to $1$ , and satisfying the equilibrium equations (the published KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$ ; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).
Normalizing constants. $b_j$ is defined through a tsum, which Lean sets to $0$ for a divergent series; every theorem assumes the series converges, the book's "none of $b_1,\dots,b_J$ is zero".
No trivial instance. The goal holds for arbitrary $I$ , $J$ , $\nu$ , routes, $\phi_j$ , $\gamma_j$ , $\delta_j$ subject only to the book's constraints; a proof for a single queue, or for fixed $\gamma=\delta$ disciplines, does not prove it. In Lemma 3.13 the function $\Phi$ is required to be positive, since $\Phi\equiv0$ satisfies (3.26) for every queue.

Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over $\prod_j \mathrm{List}(\cdot)$ , and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.

Selected references

F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://doi.org/10.2307/3212785
F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887
J. R. Jackson, Jobshop-like queueing systems, Management Science 10 (1963), 131–142. https://doi.org/10.1287/mnsc.10.1.131
F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

10 thms3 active usersReviewed

Operations Research

Missions

Feature-Based Dynamic Pricing: The EllipsoidPricing Algorithm Has Worst-Case Regret O(R d² ln(T/d))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones, in the order of the paper's argument

Significance

Difficulty

Formalization scope

Selected references

Contraction Mappings in the Theory Underlying Dynamic Programming 2: Under N-Stage Contraction and Monotonicity the Optimal Return Is the Unique Fixed Point of the Maximization OperatorResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 169)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stability and Instability of Fluid Models for Reentrant Lines 1: Every Work-Conserving Fluid Model of the Three-Buffer Line 1→2→1 Is Stable When m₁ + m₃ < 1 and m₂ < 1Research Paper

Why reentrant lines, and why this one

Setting

Formalization targets

Goal: Theorem 3.1

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case 2: General Demand: Sym-k-Concave Profit-to-Go, Optimal (s, S, A, p) PolicyResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

A Friendly Smoothed Analysis of the Simplex Method: Gaussian-Perturbed Shadows Have at Most 3 + 128πe²d²√(log n)σ⁻²(1 + 4σ√(d log n))(1 + 16σ√(log n)) Expected EdgesResearch Paper

Why the simplex method needs smoothed analysis

Setting

Formalization targets

Goal: Theorem 13 with explicit constants

Intermediate targets (milestones)

Significance

Difficulty

Formalization scope

Selected references

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.4, equation (2.3)

Milestones (PART 1 of §3)

Significance

Difficulty

Formalization scope

Selected references

Quantifying Distributional Model Risk via Optimal Transport 1: Strong Duality — the Worst-Case Expectation over an Optimal-Transport Ball on a Polish Space Equals Its Dual over (λ, φ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Airline Seat Allocation with Multiple Nested Fare Classes 2: With Integer-Valued Demands an Optimal Integer Protection-Level Policy ExistsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 132)

Milestones (in proof order)

Significance

Difficulty

Formalization scope

Selected references