Operations Research

Motivation

A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs model trust-region subproblems, max-cut and other binary programs, phase retrieval, and many problems in signal processing and control; in general they are NP-hard. The standard tool for bounding and solving them is the Shor semidefinite relaxation (Shor 1990), which lifts the variable $x$ to a matrix $Y = \begin{pmatrix}1 & x^\top\\ x & X\end{pmatrix}\succeq 0$ and replaces every quadratic term by a linear function of $Y$. The relaxation is a convex program, so it can be solved efficiently, but it is only useful when one knows that it is tight: that its optimal value equals that of the QCQP, or, more strongly, that it describes the convex hull of the QCQP's epigraph.

Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for tightness. Section 6 of the paper concerns QCQPs with symmetry: when every quadratic form is $k$ identical copies of one smaller form, $A_i = I_k\otimes\mathbb A_i$. Such problems arise as quadratic matrix programs in the sense of Beck 2007, where the variable is a matrix and the objective and constraints are traces of quadratic matrix expressions. Beck showed (Corollary 4.4) that $k\ge m$ gives value exactness under a regularity assumption; Theorem 7 of the paper gives the convex-hull result for $k\ge m+2$; this mission's Theorem 8 covers $k\ge m+1$.

Setting

Fix $N\ge 1$ variables and $m = m_I + m_E\ge 1$ constraints. For $i\in[\![0,m]\!]$ let $q_i(x) = x^\top A_ix + 2b_i^\top x + c_i$ with $A_i\in\mathbb S^N$ symmetric, $b_i\in\mathbb R^N$, $c_i\in\mathbb R$. The QCQP is

$$\mathrm{Opt} = \inf_{x\in\mathbb R^N}\{q_0(x) : q_i(x)\le 0\ (i\in[\![m_I]\!]),\ q_i(x) = 0\ (i\in[\![m_I+1,m]\!])\},$$

and its epigraph is $\mathcal D = \{(x,t) : q_0(x)\le 2t,\ x\text{ feasible}\}$.

With $Q_i = \begin{pmatrix} c_i & b_i^\top\\ b_i & A_i\end{pmatrix}$, the SDP relaxation has value

$$\mathrm{Opt}_{\mathrm{SDP}} = \inf_{x,\ X\in\mathbb S^N}\{\langle Q_0,Y\rangle : \langle Q_i,Y\rangle\le 0\ (i\le m_I),\ \langle Q_i,Y\rangle = 0\ (i> m_I),\ Y\succeq 0\},$$

and its projected epigraph $\mathcal D_{\mathrm{SDP}}$ is the set of $(x,t)$ for which some $X$ satisfies the constraints with $\langle Q_0,Y\rangle\le 2t$. Always $\operatorname{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ and $\mathrm{Opt}\ge\mathrm{Opt}_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ write $A(\gamma) = A_0+\sum_i\gamma_iA_i$ and $q(\gamma,x) = q_0(x)+\sum_i\gamma_iq_i(x)$, and let $\Gamma = \{\gamma : A(\gamma)\succeq 0,\ \gamma_i\ge 0\ \forall i\in[\![m_I]\!]\}$. Assumption 1 requires that the QCQP be feasible and that some $\gamma^*$ with $\gamma^*_i\ge 0$ on the inequalities have $A(\gamma^*)\succ 0$.

The quadratic eigenvalue multiplicity (Definition 3) is the largest integer $k$ such that $N = kn$ and every $A_i$, $i\in[\![0,m]\!]$, equals $I_k\otimes\mathbb A_i$ for some $\mathbb A_i\in\mathbb S^n$. Finally,

$$H = \{(x,t)\in\mathbb R^{N+1} : 2t = \mathrm{Opt}_{\mathrm{SDP}}\}$$

is the hyperplane on which the SDP relaxation attains its value.

Formalization targets

Goal: Theorem 8 (p. 30)

Under Assumption 1, if $k\ge m+1$, then

$$\operatorname{conv}(\mathcal D\cap H) = \mathcal D_{\mathrm{SDP}}\cap H\qquad\text{and}\qquad \mathrm{Opt} = \mathrm{Opt}_{\mathrm{SDP}}.$$

Milestones (App. B, pp. 35–36)

1. Lemma 1 (p. 7): $\mathcal D_{\mathrm{SDP}} = \{(x,t) : \sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}} = \min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Dual attainment: every $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}\cap H$ has $Z\in\mathbb S^n$ with

$$q_0(\hat x)+\langle\mathbb A_0,Z\rangle = 2\hat t,\quad q_i(\hat x)+\langle\mathbb A_i,Z\rangle\le 0\ (i\le m_I),\quad q_i(\hat x)+\langle\mathbb A_i,Z\rangle = 0\ (i>m_I),\quad Z\succeq 0.\tag{19}$$

3. Feasibility of (20): if $k\ge m+1$, some unit $y\in\mathbb R^k$ has $\langle A_i\hat x+b_i, y\otimes z\rangle = 0$ for all $i\in[\![m]\!]$.
4. The objective direction vanishes: on $\mathcal D_{\mathrm{SDP}}\cap H$, with $Z = zz^\top + Z'$, $Z'\succeq 0$, and $y$ as in (20), $\langle A_0\hat x+b_0, y\otimes z\rangle = 0$.
5. Rank induction: if $k\ge m+1$, every $(\hat x,\hat t)\in H$ with some $Z$ satisfying (19) lies in $\operatorname{conv}(\mathcal D\cap H)$.

Significance

Theorem 8 says that one copy of symmetry fewer than Theorem 7 requires still makes the SDP relaxation exact in value, and identifies the relaxation's optimal set: every optimal point of the relaxation, projected to $(x,t)$, is a convex combination of optimal epigraph points of the QCQP. In particular the relaxation's optimal points can be decomposed into QCQP optima, which is what makes the relaxation a solution method and not only a bound. Remark 14 of the paper places the result between Beck's $k\ge m$ (only $\mathcal D\cap H\ne\varnothing$) and Theorem 7's $k\ge m+2$ (the full convex hull), and records the conjecture that all three thresholds are sharp.

The theorem is proved in the paper (Appendix B). No machine-checked proof of it, or of the multiplicity results of Section 6, is known to exist. A formal proof needs a Lean development of the Shor relaxation, its Lagrangian dual, conic strong duality with dual attainment for an SDP with sign-constrained multipliers, and the Kronecker structure of the data.

Difficulty

The inclusion $\operatorname{conv}(\mathcal D\cap H)\subseteq\mathcal D_{\mathrm{SDP}}\cap H$ is routine. The converse needs, for an SDP-optimal point, a decomposition into feasible QCQP points that are themselves optimal. A rank-one decomposition of the SDP matrix $X - xx^\top$ does not suffice in general: its terms leave the feasible set unless the perturbation directions are orthogonal to all the linear parts $A_i\hat x+b_i$, including the objective's. With multiplicity $k\ge m+2$ there is room for all $m+1$ orthogonality conditions; with $k\ge m+1$ only the $m$ constraint conditions can be imposed, and the objective condition has to come from elsewhere. The difficulty sits in that last condition and in the conic duality step, whose dual must attain its value under Assumption 1 alone (no polyhedrality of $\Gamma$, no attainment assumption).

Formalization scope

The Lean development lives in the namespace QCQPTightness.MultTight. The data are a structure QCQP N m with symmetric $A_i$, constraints indexed by Fin m, and constraint i an inequality exactly when (i : ℕ) < mI (the paper's inequalities come first). Vectors are Fin N → ℝ; points of $\mathbb R^{N+1}$ are pairs (x, t). $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, and $H$ is defined from that EReal value; this is why the goal states $\mathrm{Opt} = \mathrm{Opt}_{\mathrm{SDP}}$ as a separate conjunct: if $\mathrm{Opt}_{\mathrm{SDP}}$ were $\pm\infty$, $H$ would be empty and the first conjunct trivial. $\langle Q,Y\rangle$ is (Q * Y).trace; $Y\succeq 0$ is PosSemidef; $\mathbf S^{k-1}$ is y ⬝ᵥ y = 1. The identification $\mathbb R^k\otimes\mathbb R^n\cong\mathbb R^N$ sends block $j$, entry $s$ to coordinate s + n * j.

Standing assumptions: the goal carries $m\ge 1$ (p. 1) and Assumption 1. The multiplicity is the largest $k$ (IsGreatest), as on the page. The milestones take an explicit representation $A_i = I_k\otimes\mathbb A_i$ instead, which makes them apply to every representation, and drop $m\ge 1$ and Assumption 1 where the step does not use them. The rank-induction milestone carries $(\hat x,\hat t)\in H$, which the page's sentence omits but its proof uses ("by minimality of $\hat t$"); without it the claim is false.

A trivializing formalization would assume system (19), or the vanishing of $\langle A_0\hat x+b_0, y\otimes z\rangle$, in the goal; the goal assumes neither, and both are milestones to be proved.

Reusable infrastructure: the QCQP and Shor-relaxation definitions are shared with the other missions of this series, and a general SDP strong-duality statement exists on the platform (ConvexOptimization.sdp_strong_duality) in a different form (a minimization without sign-constrained variables). Contributions welcome: proofs of the milestones, a conic duality lemma with sign-constrained multipliers, and Kronecker-product lemmas such as $(I_k\otimes\mathbb A)(y\otimes z) = y\otimes\mathbb Az$.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Math. Program. (2021); arXiv:1911.09195v3 (2020). https://arxiv.org/abs/1911.09195, https://doi.org/10.1007/s10107-020-01589-9
• A. Beck, Quadratic matrix programming, SIAM J. Optim. 17(4):1224–1238, 2007. https://doi.org/10.1137/050644471
• N. Z. Shor, Dual quadratic estimates in polynomial and boolean programming, Ann. Oper. Res. 25:163–168, 1990.
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, J. Global Optim. 10(4):367–380, 1997.

Motivation

Car dealers, electronics retailers and office suppliers sell products whose prices and features are set upstream by manufacturers, and bundle each product with a service of their own: maintenance, repairs or a warranty. The dealer's short-term problem is then purely combinatorial. Which products should be carried, and which of them should come with a long rather than a short service? Longer service makes a product more attractive to consumers but costs the dealer more per unit sold, and the cost per unit of service time depends on the product's quality.

Wang, Ke and Cui (SSRN 3766191, accepted at Manufacturing & Service Operations Management) study price, quality and service decisions under multinomial logit (MNL) and nested logit demand. Section 5.2 of the paper treats the dealer's problem and shows that its solution has a two-threshold structure. This mission formalizes that result, Theorem 5, together with the steps of its proof in the Online Supplement.

The single-service version of the question is classical: under MNL demand with fixed prices, the profit-maximizing assortment consists of the products with the highest margins, a revenue-ordered (here: markup-ordered) assortment (Talluri & van Ryzin 2004). Theorem 5 extends this to two service options per product, where the choice is between three actions for each product (not offered, short service, long service) and the margin of each action differs.

Setting

There are products $\mathcal N=\{1,\dots,N\}$. Product $i$ has a fixed price $p_i$ and quality $q_i$, a quality sensitivity $\alpha_i$, a service utility per unit time $s_i$, a unit production cost $c_iq_i^2$, and a service cost per unit time $a_i-b_iq_i$. Two service durations are available: a short one $t_s$ and a long one $t_l$.

The dealer chooses two disjoint sets $S_l,S_s\subseteq\mathcal N$: products in $S_l$ are offered with service duration $t_l$, products in $S_s$ with $t_s$, and the others are not offered. A product $i$ offered with duration $t$ has attraction $\exp(\alpha_iq_i-p_i+ts_i)$ and markup $p_i-c_iq_i^2-t(a_i-b_iq_i)$. Under MNL demand with an outside option, product $i\in S_l$ is bought with probability

$$d_i(\mathbf p,\mathbf q;S_l,S_s)=\frac{\exp(\alpha_iq_i-p_i+t_ls_i)}{1+\sum_{j\in S_l}\exp(\alpha_jq_j-p_j+t_ls_j)+\sum_{j\in S_s}\exp(\alpha_jq_j-p_j+t_ss_j)},$$

and similarly with $t_s$ for $i\in S_s$ (eq. (12)). The dealer's expected profit, with market size one, is

$$\Pi^s(\mathbf p,\mathbf q;S_l,S_s)=\sum_{i\in S_l}\big[p_i-c_iq_i^2-t_l(a_i-b_iq_i)\big]d_i+\sum_{i\in S_s}\big[p_i-c_iq_i^2-t_s(a_i-b_iq_i)\big]d_i ,$$

and problem (13) is to maximize $\Pi^s$ over disjoint pairs $(S_l,S_s)$.

Two orderings of products appear in the answer. The short-service markup is $z_i=p_i-c_iq_i^2-t_s(a_i-b_iq_i)$. The adjusted markup is

$$x_i=(p_i-c_iq_i^2)-A_i\,(a_i-b_iq_i),\qquad A_i=\frac{t_l\exp(t_ls_i)-t_s\exp(t_ss_i)}{\exp(t_ls_i)-\exp(t_ss_i)} .$$

A markup-ordered assortment is a set of the products with the highest values of $z_i$; an adjusted markup-ordered set is a set of the products with the highest values of $x_i$.

Formalization targets

Goal: Theorem 5

Assume $t_s<t_l$, $s_i>0$ and $a_i-b_iq_i\ge0$ for all $i$. There are thresholds $\theta,\theta'$ such that, with $S_{i^*}=\{i:z_i\ge\theta\}$ and $S_{j^\natural}=\{i:x_i\ge\theta'\}$,

$$S_{j^\natural}\subseteq S_{i^*}\quad\text{and}\quad \Pi^s(\mathbf p,\mathbf q;S_l,S_s)\le\Pi^s\big(\mathbf p,\mathbf q;S_{j^\natural},\,S_{i^*}\setminus S_{j^\natural}\big)\ \text{ for all disjoint }(S_l,S_s).$$

Part (a) of the paper (a markup-ordered assortment is an optimal offer set) and part (b) (long service on an adjusted markup-ordered subset of it, short service on the rest) are one statement about the same $S_{i^*}$.

Milestones from the proof (Online Supplement p. 8)

1. (EC.11). For disjoint $(S_l,S_s)$, $r=\Pi^s(S_l,S_s)$ if and only if $r=\sum_{i\in S_l}h^l_i(r)+\sum_{i\in S_s}h^s_i(r)$, where $h^l_i(r)=[y_i-r]\exp(\alpha_iq_i-p_i+t_ls_i)$, $h^s_i(r)=[z_i-r]\exp(\alpha_iq_i-p_i+t_ss_i)$ and $y_i=p_i-c_iq_i^2-t_l(a_i-b_iq_i)$.
2. The fixed point. $H(r)=\max_{S_l,S_s}\{\sum_{S_l}h^l_i(r)+\sum_{S_s}h^s_i(r)\}=\sum_i\max\{h^l_i(r),h^s_i(r),0\}$; $H$ is non-increasing; $r=H(r)$ has a unique root $r^*$, and $r^*$ is the optimal value of (13).
3. Breakpoints. $x_i,y_i,z_i$ are the roots of $h^l_i=h^s_i$, $h^l_i=0$, $h^s_i=0$, and $x_i\le y_i\le z_i$.
4. Piecewise form. $h_i=h^l_i$ on $r\le x_i$, $h^s_i$ on $x_i<r\le z_i$, $0$ on $r>z_i$.
5. Level sets at $r^*$. $S_l=\{x_i\ge r^*\}$ and $S_s=\{z_i\ge r^*\}\setminus S_l$ is an optimal pair with profit $r^*$.

Significance

Problem (13) has $3^N$ feasible pairs. Theorem 5 reduces the search to at most $O(N^2)$ pairs indexed by two thresholds, and it says which products deserve the long service: those with the highest adjusted margin $x_i$, which charges each unit of service cost at the rate $A_i>t_l$ rather than at $t_l$. The paper's managerial reading is that high-margin products go with long service, as with retailers that attach longer warranties to expensive items.

The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified two-service extension of the MNL revenue-ordered assortment theorem, and the fixed-point reduction (milestones 1 and 2) is a reusable device for MNL assortment problems with several options per product.

Difficulty

The profit is a ratio of sums, so exchanging one product's service changes every choice probability, and pairwise exchange arguments do not directly compare assortments. The naive idea of ranking products by a single margin fails: the long-service margin $y_i$ and the short-service margin $z_i$ order products differently, and the long service also raises the product's attraction. Neither ordering alone decides which products get long service. The adjusted markup $x_i$ is the breakpoint at which long and short service become equally profitable, and the three breakpoints $x_i\le y_i\le z_i$ must line up for the threshold structure to hold. This ordering uses $a_i-b_iq_i\ge0$: with a negative service cost the long service can be optimal for a product whose adjusted markup is below that of a product left unserved, and part (b) fails.

Formalization scope

• Products are Fin N (0-based); $N=0$ is allowed. All parameters $\alpha,a,b,c,s,p,q$ are arbitrary real vectors and $t_s,t_l$ real numbers; prices and qualities are fixed data, not decisions.
• The outside option is the constant $1$ in the denominator. The MNL formula is the definition; its derivation from Gumbel utilities is cited, not formalized.
• Decisions are pairs of Finset (Fin N) with Disjoint Sl Ss; optimality is a global inequality against every disjoint pair.
• "Markup-ordered" and "adjusted markup-ordered" are upper level sets $\{i: z_i\ge\theta\}$, $\{i:x_i\ge\theta'\}$ with real thresholds. Each is a prefix of every decreasing relabelling, so no tie-break is fixed; the empty and the full set are allowed.
• The model's standing assumptions are explicit hypotheses wherever they are used: $t_s<t_l$ (shortest and longest duration), $s_i>0$ (service utility) and $a_i-b_iq_i\ge0$ (service cost). The first two make $A_i$ well defined; $A_i$ is a total Lean function that returns $0$ when its denominator vanishes, a value no statement relies on. No sign is imposed on $b_i$ or $c_i$.
• Trivializing formalizations are ruled out: the statement has two service levels (a single level would be the Talluri–van Ryzin theorem), uses level sets rather than a fixed relabelling with strict orders, ties the long-service set to the same offered set in (a) and (b) instead of using independent existentials, and states the three hypotheses rather than leaving them implicit.
• Definitions: the MNL choice probabilities and profit (12)–(13), and the auxiliary functions $h^l_i,h^s_i,h_i,H$, $A_i$, $x_i$. Proofs of the milestones need only finite sums, max and elementary real analysis. Proofs of any milestone, and alternative routes to Theorem 5, are welcome.

Selected references

• Ruxian Wang, Chenxu Ke, Shiliang Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022 (accepted manuscript, SSRN 3766191). https://ssrn.com/abstract=3766191 — DOI of the published version: https://doi.org/10.1287/msom.2020.0947
• Kalyan Talluri, Garrett van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• Daniel McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.

Motivation

A firm that sells durable products with an attached service (a warranty, a maintenance plan, a support contract) chooses three things for each product: its price, its quality, and how long the service lasts. Wang, Ke and Cui (SSRN 3766191, Manufacturing & Service Operations Management, 2022) study this joint decision when consumers choose among the products according to a discrete choice model. Under the multinomial logit (MNL) model they show that every product's optimal service duration is either the shortest or the longest available, so that the products split into a short-service group and a long-service group.

That conclusion suggests a different model of the consumer. In business procurement, and more generally when the buyer first decides how long a product will be used, the consumer plausibly chooses a service duration first and a product second. The two-stage nested logit (NL) model (Ben-Akiva 1973; McFadden 1980) captures exactly this: the two service groups become nests, and products within a nest are closer substitutes than products in different nests. Section 4 of the paper asks whether the MNL structure of optimal qualities and prices survives in this model. This mission formalizes its answer, Theorem 4.

Price optimization under the nested logit model has a substantial literature. For prices alone, the optimal prices within a nest share one markup and the problem reduces to a one-dimensional fixed point (Li & Huh 2011; Gallego & Wang 2014). Theorem 4 adds quality as a decision, with production cost quadratic in quality and service cost depending on quality.

Setting

There are two nests $x\in\{s,l\}$. Nest $x$ contains $m_x$ products $i=1,\dots,m_x$, and every product of nest $x$ is sold with the same fixed service duration $t_x$. Product $i$ of nest $x$ has parameters $\alpha_{xi}$ (quality sensitivity), $a_{xi}$ (base service cost per unit time), $b_{xi}$ (marginal effect of quality on service cost), $c_{xi}>0$ (production-cost coefficient) and $s_{xi}$ (service utility per unit time). The firm chooses a price $p_{xi}$ and a quality $q_{xi}$ for every product.

The total attractiveness of nest $x$ is $e_x=\sum_{i=1}^{m_x}\exp(\alpha_{xi}q_{xi}-p_{xi}+t_xs_{xi})$. With upper-level scale parameter $\mu_1\ge 1$ (the nest coefficient is $1/\mu_1$; the lower-level scale is normalized to $1$), a consumer chooses nest $x$ with probability

$$d_x(\mathbf p,\mathbf q)=\frac{e_x^{1/\mu_1}}{1+e_s^{1/\mu_1}+e_l^{1/\mu_1}},$$

buys nothing with the remaining probability, and, having chosen nest $x$, picks product $i$ with probability $d_{i|x}=\exp(\alpha_{xi}q_{xi}-p_{xi}+t_xs_{xi})/e_x$. The probability of buying product $i$ of nest $x$ is $d_{xi}=d_x\,d_{i|x}$. The markup of a product is its price minus production cost $c_{xi}q_{xi}^2$ minus service cost $t_x(a_{xi}-b_{xi}q_{xi})$, and the firm's expected profit (market size one) is

$$\Pi_M(\mathbf p,\mathbf q)=\sum_{x\in\{s,l\}}\sum_{i=1}^{m_x}\bigl[p_{xi}-c_{xi}q_{xi}^2-t_x(a_{xi}-b_{xi}q_{xi})\bigr]\,d_{xi}(\mathbf p,\mathbf q).$$

The firm maximizes $\Pi_M$ over all real price and quality vectors. When $\mu_1=1$ the model is the MNL model.

Formalization targets

Goal: Theorem 4

Let $q^\dagger_{xi}=(\alpha_{xi}+t_xb_{xi})/(2c_{xi})$. The equation

$$r=\sum_{x\in\{s,l\}}\mu_1\Bigl(\sum_{i=1}^{m_x}\exp\bigl(\alpha_{xi}q^\dagger_{xi}-c_{xi}q^{\dagger2}_{xi}-t_x(a_{xi}-b_{xi}q^\dagger_{xi})+t_xs_{xi}-r-\mu_1\bigr)\Bigr)^{1/\mu_1}$$

has a unique real solution $r^\dagger$. With $p^\dagger_{xi}=\mu_1+r^\dagger+c_{xi}q^{\dagger2}_{xi}+t_x(a_{xi}-b_{xi}q^\dagger_{xi})$,

$$\Pi_M(\mathbf p,\mathbf q)\le\Pi_M(\mathbf p^\dagger,\mathbf q^\dagger)=r^\dagger\quad\text{for all }(\mathbf p,\mathbf q),$$

and $(\mathbf p^\dagger,\mathbf q^\dagger)$ is the only maximizer.

Milestones

The milestones follow the paper's proof in the Online Supplement:

1. (EC.5): at an optimal price vector, every product $i$ of nest $x$ has markup $1+r/\mu_1+(1-1/\mu_1)r_x$, where $r$ is the profit and $r_x$ the nest's average markup; so markups are constant within a nest.
2. (EC.6): with a common markup $\rho_x$ per nest, the profit is $\sum_x\rho_x d_x(\boldsymbol\rho,\mathbf q)$; at the optimal markups, $\rho_x-\mu_1=r$ for each nonempty nest.
3. (EC.7): for every $r$, the right-hand side above, as a function of $\mathbf q$, is maximized exactly at $\mathbf q^\dagger$.
4. (EC.8): that right-hand side is strictly decreasing in $r$, so the fixed-point equation has exactly one root.

Significance

The result. Theorem 4 has two consequences. First, each product's optimal quality depends only on its own parameters and its nest's service duration, not on any other product, although all products are substitutes. At this quality, the marginal production and service cost of quality equals the consumer's marginal utility from it. Second, every product in both nests carries the same markup, $\mu_1+r^\dagger$: the optimal profit plus the reciprocal of the nest coefficient. A pricing problem with $m_s+m_l$ prices reduces to finding the root of a single monotone function. Proposition 7 of the paper uses these closed forms to compare consumer surplus with and without quality control under the NL model.

Formalizing it. The paper's proof writes down first-order conditions and assumes an optimum exists. The goal here is global optimality and uniqueness over all real prices and qualities, which the paper does not prove. A complete formalization needs the existence of the maximizer or a direct upper bound, together with the first-order identities. The related platform item DLevelNestedLogit.Pricing.stationary_point_iff (Li et al. 2015) characterizes stationary points of the price-only revenue in a $d$-level nested logit model. It has no costs and no quality, and it is not used here. No result of this mission has a machine-checked proof yet.

Difficulty

The profit $\Pi_M$ is not concave in prices (under the nested logit model, concavity is known only after a change of variables to market shares, Li & Huh 2011), so a first-order condition does not by itself certify a global maximum. The paper's argument shows only that any optimum satisfies the stated formulas. For a global result, the critical points must be shown to coincide with the maximizers, and the profit must be bounded above by $r^\dagger$ everywhere, including at decisions where markups differ across products of a nest or are negative. The two reductions, to nest markups and then to the scalar $r$, are only valid at the optimum and have to be carried out with that in mind. The exponent $1/\mu_1\le 1$ makes $e_x^{1/\mu_1}$ concave rather than linear in the nest attractiveness. This is the step where the MNL argument does not transfer verbatim.

Formalization scope

• Nests are a two-element type Nest (s, l). Products of nest $x$ are Fin (m x), 0-based. Nests may be empty: an empty nest has $e_x=0$, $0^{1/\mu_1}=0$, and contributes nothing.
• The outside option is the "$1+$" in the denominator of $d_x$, not a nest.
• Durations $t_s,t_l$ are fixed data, not decisions, with no order assumed between them. The nests are fixed.
• Prices and qualities range over all of $\mathbb R$. The model's normalization $q\ge 0$ is not imposed, as in the paper's own formula.
• Standing hypotheses: $\mu_1\ge 1$ (general; $\mu_1=1$ is allowed but is not the only case) and $c_{xi}>0$. No sign is imposed on $\alpha,a,b,s$.
• Powers are Real.rpow of nonnegative sums of exponentials.
• "Optimal" means a global maximizer over all real vectors. The milestones that the paper derives from first-order conditions are stated as properties of a global maximizer.
• The price formula $p^\dagger$ takes $r$ as an argument, and the theorem must identify $r=r^\dagger$.

The following versions are trivializing and are excluded: $\mu_1=1$ only (the MNL case), a single nest, first-order conditions in place of global optimality, fixed qualities, or an optimum defined by the paper's formula.

The definitions (Model, MarkupProblem, Optimum) are self-contained and can be reused for other nested logit pricing results. Contributions are welcome on each milestone, on a sorry-free derivative of $\Pi_M$ in $p_{xi}$, and on an existence result for the maximizer.

Selected references

• Y. Wang, J. Ke, S. Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022 (accepted manuscript, SSRN 3766191). https://ssrn.com/abstract=3766191 — DOI https://doi.org/10.1287/msom.2020.0947
• M. Ben-Akiva, Structure of Passenger Travel Demand Models, PhD thesis, Massachusetts Institute of Technology, 1973 (no stable link; cited as in the source's bibliography).
• D. McFadden, Econometric Models for Probabilistic Choice Among Products, Journal of Business 53(3), S13–S29, 1980. https://doi.org/10.1086/296093
• H. Li, W. T. Huh, Pricing Multiple Products with the Multinomial Logit and Nested Logit Models: Concavity and Implications, Manufacturing & Service Operations Management 13(4), 549–564, 2011. https://doi.org/10.1287/msom.1110.0344
• G. Gallego, R. Wang, Price Optimization and Competition for Multi-Products under the Nested Logit Model with Product-Differentiated Price Coefficients, Operations Research 62(2), 450–461, 2014 (cited as in the source's bibliography; link not verified in this session).

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model facility location, pooling, max-cut, trust-region steps and robust optimization problems, and every $\{0,1\}$ integer program can be written as one; in general they are NP-hard. The standard tractable approach is the Shor semidefinite relaxation, which lifts $x$ to the matrix $xx^\top$ and relaxes the rank-one condition to positive semidefiniteness. A recurring question is when this relaxation loses nothing: when its optimal value equals that of the QCQP (SDP tightness), and, more strongly, when its projected epigraph equals the convex hull of the QCQP's epigraph (convex hull exactness). The second property also describes the convex hull of the nonconvex feasible set's epigraph, which is useful in branch-and-bound and cutting-plane methods.

Timeline. The S-lemma (Yakubovich, 1971) gives SDP tightness for one inequality constraint, and Fujie and Kojima (1997) recorded the dual description of the SDP value used below. For the trust-region subproblem and its generalization, convex hull descriptions of the epigraph were given by Ho-Nguyen and Kılınç-Karzan (2017) and by Wang and Kılınç-Karzan (arXiv:1907.08843, 2019). Beck (2007) and Beck, Drori and Teboulle (2012) gave SDP tightness results for quadratic matrix programs. Wang and Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (arXiv:1911.09195v3, Math. Program. 2021), introduced a general framework based on the faces of a dual set $\Gamma$ and proved convex hull and tightness results for polyhedral $\Gamma$ and for QCQPs with large quadratic eigenvalue multiplicity. This mission formalizes the paper's first convex hull theorem (Theorem 1, p. 13) and the framework it rests on.

Setting

Fix $N$ variables and $m\ge1$ constraints, the first $m_I$ inequalities and the remaining $m_E=m-m_I$ equalities. Each function is

$$q_i(x)=x^\top A_ix+2b_i^\top x+c_i,\qquad A_i\in\mathbb S^N,\ b_i\in\mathbb R^N,\ c_i\in\mathbb R,\quad i=0,\dots,m.$$

The QCQP (1) is $\mathrm{Opt}=\inf\{q_0(x): q_i(x)\le0\ (i\le m_I),\ q_i(x)=0\ (i>m_I)\}$, and its epigraph is $\mathcal D=\{(x,t): x\text{ feasible},\ q_0(x)\le2t\}$.

With $Q_i=\begin{pmatrix}c_i&b_i^\top\\ b_i&A_i\end{pmatrix}$ and $Y=\begin{pmatrix}1&x^\top\\ x&X\end{pmatrix}$, the SDP relaxation (3) minimizes $\langle Q_0,Y\rangle$ over $X\in\mathbb S^N$ with $Y\succeq0$ and the constraints $\langle Q_i,Y\rangle\le0$ or $=0$; its value is $\mathrm{Opt}_{\mathrm{SDP}}$ and its projected epigraph is $\mathcal D_{\mathrm{SDP}}=\{(x,t):\exists X,\ (x,X)\text{ feasible},\ \langle Q_0,Y\rangle\le2t\}$ (4). Always $\mathrm{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ and $\mathrm{Opt}\ge\mathrm{Opt}_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ let $A(\gamma)=A_0+\sum_i\gamma_iA_i$, and similarly $b(\gamma)$, $c(\gamma)$ and the Lagrangian $q(\gamma,x)=q_0(x)+\sum_i\gamma_iq_i(x)$. The dual object is

$$\Gamma=\{\gamma\in\mathbb R^m:\ A(\gamma)\succeq0,\ \gamma_i\ge0\ \text{for } i\le m_I\}.$$

Assumption 1: the QCQP is feasible and some $\gamma^*$ with $\gamma^*_i\ge0$ for $i\le m_I$ has $A(\gamma^*)\succ0$. Assumption 3: $\Gamma$ is polyhedral. For $\hat x\in\mathbb R^N$, $\mathcal F(\hat x)=\arg\max_{\gamma\in\Gamma}q(\gamma,\hat x)$. A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$ and semidefinite otherwise, with shared zero eigenspace $\mathcal V(\mathcal F)=\{v: A(\gamma)v=0\ \forall\gamma\in\mathcal F\}$. Finally $\operatorname{aff\,dim}$ denotes affine dimension.

Formalization targets

Goal: Theorem 1 (p. 13)

Under Assumptions 1 and 3, if every semidefinite face $\mathcal F$ of $\Gamma$ satisfies $\dim\mathcal V(\mathcal F)\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$, then

$$\mathrm{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}\qquad\text{and}\qquad\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}.$$

Milestones

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}}=\{(x,t):\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}}=\min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Lemma 2 (p. 9): a semidefinite face has a unit vector in $\mathcal V(\mathcal F)$.
3. Lemma 3 (p. 9): under Assumptions 1 and 2, a point of $\mathcal D_{\mathrm{SDP}}$ with definite $\mathcal F(\hat x)$ lies in $\mathcal D$.
4. Observation 1 (p. 10): under Assumption 1, a face of affine dimension $m$ is definite.
5. Lemma 4 (p. 10): under Assumptions 1, 2 and the decomposition condition (7), the two conclusions of Theorem 1 hold.
6. Lemma 8 (p. 13): under Assumption 3, $\Gamma=\Gamma_e+\mathrm{cone}(\Gamma_r)$ with polytopes $\Gamma_e,\Gamma_r$, and $\mathcal F(\hat x)=\mathcal F_e(\hat x)+\mathrm{cone}(\mathcal F_r(\hat x))$ when the supremum is finite.
7. Lemma 7 (p. 13): under the hypotheses of Theorem 1, condition (7) holds.

Companions

Lemma 6 (p. 11: $\dim\mathcal V(\mathcal F)\ge k$ for the quadratic eigenvalue multiplicity $k$), Theorem 2 (p. 15: the hypothesis of Theorem 1 with $k$ in place of $\dim\mathcal V(\mathcal F)$), and Corollaries 1–4 (pp. 16–18: convex quadratic programs, one constraint, $b_i=0$, scalar quadratic forms with $m\le N$).

Significance

The result. Theorem 1 gives a checkable sufficient condition, stated on the faces of a polyhedral dual set, under which the Shor relaxation is exact in the strongest sense: it describes $\mathrm{conv}(\mathcal D)$, so the SDP value equals the QCQP value and, by Remark 7, $\mathrm{conv}(\mathcal D)$ is second-order cone representable. Through Lemma 6 it becomes Theorem 2, the symmetry condition $k\ge\operatorname{aff\,dim}\{b(\gamma)\}+1$; its corollaries recover the convex hull results for the trust-region subproblem and its generalization and give new ones for simultaneously diagonalizable and "Swiss cheese" problems. The sharpness of the bound is shown in §4.3 of the paper.

Formalizing it. The theorem is proved in the paper; nothing in it is machine-checked. A formal proof needs strong conic duality for the SDP in Lemma 1, the Minkowski–Weyl decomposition in Lemma 8, and the face-by-face decomposition argument of Lemma 7. These pieces are shared with the paper's SDP tightness result (Theorem 3), which uses Lemmas 1–3 and 8 again.

Difficulty

The obvious attempt is to take $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}$, recover a rank-one solution of the SDP, and read off a point of $\mathcal D$. This fails because an optimal $Y$ need not have rank one, and a rank-reduction step can leave the feasible set of a nonconvex constraint. The paper instead moves $(\hat x,\hat t)$ along a direction $v$ in the shared zero eigenspace of the face $\mathcal F(\hat x)$, and must show that both endpoints of the move stay in $\mathcal D_{\mathrm{SDP}}$ while the face strictly grows in affine dimension. Controlling the endpoints needs finiteness of the relevant family of quadratic functions, which is where polyhedrality enters; without it (§4.3) the argument and the theorem fail. Lemma 1 also needs a strong duality theorem for semidefinite programs with a minimax step, neither of which is elementary in Lean.

Formalization scope

The Lean development lives in the namespace QCQPTightness.ConvHull. A QCQP is a structure with symmetric $A_0, A_i$, vectors $b_0,b_i$, scalars $c_0,c_i$ and a count $m_I\le m$; constraints are indexed by Fin m, constraint $i$ being an inequality exactly when $i<m_I$. Conventions:

• $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, never real infima; points of $\mathbb R^{N+1}$ are pairs $(x,t)$, and $\mathrm{conv}$ is convexHull ℝ.
• Faces of $\Gamma$ are nonempty convex extreme subsets; the page's convention $\operatorname{aff\,dim}\emptyset=-1$ makes the empty face irrelevant, while Lean's affine dimension of $\emptyset$ would be $0$.
• "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t$" is written $\forall\gamma\in\Gamma,\ q(\gamma,x)\le2t$; "a convex combination of points with property $P$" is membership in the convex hull of the set of such points; the unit sphere is $v^\top v=1$.
• The goal carries exactly the paper's hypotheses plus its standing assumption $m\ge1$ (p. 1); Assumption 2 is not assumed because Assumption 3 implies it.
• Lemma 8 is printed with "$\mathcal F_r(\hat x)$ is the face of $\Gamma_e$"; it is formalized with $\Gamma_r$, as the proof and Lemma 7 use it.

A trivializing formalization would assume condition (7), the decomposition of Lemma 8, or any property of $\mathcal F(\hat x)$ in the goal; the goal assumes none of these, and the dimension hypothesis is satisfiable with semidefinite faces present (for $q_0=-x^2$, $q_1=x^2-1$, the face $\{\gamma_1=1\}$ is semidefinite with $\dim\mathcal V=1$).

Infrastructure needed: SDP strong duality (the platform has ConvexOptimization.sdp_strong_duality), the Minkowski–Weyl theorem for polyhedra, faces of convex sets and affine dimension. Proofs of any milestone, of the companions, and reusable lemmas about faces of spectrahedra are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Math. Program. (2021); arXiv:1911.09195v3. https://arxiv.org/abs/1911.09195 , https://doi.org/10.1007/s10107-020-01589-9
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, J. Global Optim. 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
• A. Beck, Quadratic matrix programming, SIAM J. Optim. 17 (2007) 1224–1238. https://doi.org/10.1137/05064816X
• N. Ho-Nguyen, F. Kılınç-Karzan, A second-order cone based approach for solving the trust-region subproblem and its variants, SIAM J. Optim. 27 (2017) 1485–1512. https://doi.org/10.1137/16M1065197
• A. L. Wang, F. Kılınç-Karzan, The generalized trust region subproblem: solution complexity and convex hull results, arXiv:1907.08843 (2019). https://arxiv.org/abs/1907.08843
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X

Motivation

In online matching with multiple prices, a firm sells $n$ items with limited inventories to customers who arrive one at a time; each item can be offered at any price from its own finite price set, and the firm must commit to an offer without knowing future customers. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020) show that the best possible competitive ratio (worst-case ratio of the online revenue to the offline LP optimum) for a price set $\mathcal P$ is an explicit number $F(\mathcal P) = 1 - e^{-\alpha^{(1)}}$, computed from $\mathcal P$ alone.

Two tight ratios were known before. For a single item sold over a price set, Ball and Queyranne (Oper. Res. 2009) found the tight ratio $\sigma^{(1)}$. For many items with one price each, the tight ratio is $1 - 1/e$ (Karp, Vazirani and Vazirani 1990; Mehta, Saberi, Vazirani and Vazirani 2007). For a single item whose price ranges over a continuum $[r^{(1)}, r^{(m)}]$, Ball and Queyranne give $1/(1 + \ln(r^{(m)}/r^{(1)}))$. A reader meeting $F(\mathcal P)$ for the first time asks how it compares with these. Proposition 2 of the paper answers that question with strict inequalities, and this mission formalizes it.

Setting

A price set consists of $m$ prices

$$0 < r^{(1)} < r^{(2)} < \dots < r^{(m)},$$

with the convention $r^{(0)} := 0$. Write $s_j = r^{(j-1)}/r^{(j)} \in (0,1)$ for $j = 2, \dots, m$.

The booking limits $\alpha^{(1)}, \dots, \alpha^{(m)}$ are positive numbers with $\sum_j \alpha^{(j)} = 1$ satisfying

$$1 - e^{-\alpha^{(1)}} = \frac{1 - e^{-\alpha^{(j)}}}{1 - s_j}, \qquad j = 2, \dots, m. \qquad (7)$$

The Ball–Queyranne limits $\sigma^{(1)}, \dots, \sigma^{(m)}$ are positive numbers with $\sum_j \sigma^{(j)} = 1$ satisfying

$$\sigma^{(1)} = \frac{\sigma^{(j)}}{1 - s_j}, \qquad j = 2, \dots, m. \qquad (8)$$

Both systems have exactly one solution (Proposition 1). The paper's ratios are $F(\mathcal P) = 1 - e^{-\alpha^{(1)}}$ and $G(\mathcal P) = \sigma^{(1)}$ (Definition 2). Finally, for $m \ge 2$ let $\alpha$ be the unique real root of

$$1 - e^{-\alpha} = \frac{1 - \alpha}{\ln(r^{(m)}/r^{(1)})};$$

$1 - e^{-\alpha}$ is the paper's competitive ratio when every item may be priced anywhere in $[r^{(1)}, r^{(m)}]$ (App. E.1).

In Lean the prices are r : ℕ → ℝ read at $1, \dots, m$, and IsPriceSet m r, IsBookingLimits m r α, IsBQLimits m r σ are the predicates above.

Formalization targets

Goal: Proposition 2 (p. 17)

For $m \ge 2$,

$$\Bigl(1 - \frac1e\Bigr)\sigma^{(1)} < 1 - e^{-\sigma^{(1)}} < 1 - e^{-\alpha^{(1)}}, \qquad (11)$$ $$\frac{1}{1 + \ln(r^{(m)}/r^{(1)})} < \sigma^{(1)}, \qquad (12)$$ $$1 - e^{-\alpha} < 1 - e^{-\alpha^{(1)}}. \qquad (13)$$

Milestones

1. Proposition 1 (p. 13): existence and uniqueness of the solutions of (7) and of (8).
2. Explicit $\sigma$ (App. A, p. 38): $\sigma^{(j)} = (1 - r^{(j-1)}/r^{(j)})\bigl(1 + \sum_{j'=2}^m (1 - s_{j'})\bigr)^{-1}$.
3. Monotonicity (App. A, p. 38): $x \mapsto x/(1 - e^{-x})$ (with its limit value $1$ at $x = 0$) is strictly increasing on $[0, 1]$.
4. (33) (App. A, p. 39): $\alpha^{(1)}$ is the unique solution of $x + \sum_{j=2}^m -\ln\bigl(1 - (1 - e^{-x})(1 - s_j)\bigr) = 1$.
5. (34) (App. A, p. 39): the root $\alpha$ is the unique solution of $x + \sum_{j=2}^m (1 - e^{-x})\ln(r^{(j)}/r^{(j-1)}) = 1$, and it lies in $(0,1)$.
6. Ranges of $F$ and $G$ (p. 14): $1 - e^{-1/m} \le F(\mathcal P) \le 1 - e^{-1}$ and $1/m \le G(\mathcal P) \le 1$.
7. Two prices, (4) (p. 7): for $\mathcal P = \{r, \xi r\}$, $F(\mathcal P) = 1 - \bigl(\sqrt{1 + 4\xi(\xi-1)/e} - 1\bigr)/(2(\xi - 1))$.

Significance

The result. Inequality (11) shows that the multi-item, multi-price ratio is not obtained by multiplying the single-item ratio $\sigma^{(1)}$ by the single-price penalty $1 - 1/e$: the true ratio is strictly larger, so neither the ratio nor the algorithms of the paper can be assembled from the two classical cases. Inequalities (12) and (13) quantify the value of a discrete price menu: restricting the continuum $[r^{(1)}, r^{(m)}]$ to finitely many prices strictly raises the tight ratio, both for one item (Ball–Queyranne) and for many items (this paper). The ranges of $F$ and $G$ bound the guarantees in terms of the number of prices alone, and the two-price formula (4) is the explicit instance used throughout the paper's introduction.

Formalizing it. All results here are proved in the paper (App. A); none has a machine-checked proof that we know of. The mission produces a checked theory of the booking-limit systems (7) and (8), which the paper's three main theorems (the competitive ratios of Multi-price Balance and Multi-price Ranking, and the matching upper bound) all rest on, and checked proofs of the comparisons. The booking-limit predicates are the same in the companion missions of this series and are intended to be shared after consolidation.

Difficulty

The statements are elementary, but (7) is a nonlinear system: eliminating $\alpha^{(2)}, \dots, \alpha^{(m)}$ leaves a polynomial equation of degree $m$ in $e^{-\alpha^{(1)}}$, with no closed form for $m \ge 3$. So $\alpha^{(1)}$ cannot be computed and compared directly; every inequality has to be derived from properties of the defining equations. The root $\alpha$ of (13) is likewise defined only implicitly (via the Lambert $W$ function). The naive approach of comparing the two systems equation by equation does not give (11)'s second inequality, because (7) and (8) relate each limit to the first one through different functions and the two families are tied together only by their common normalization $\sum_j = 1$. In Lean the main friction is bookkeeping: sums over $\{2, \dots, m\}$, natural-number index arithmetic $j - 1$, and the uniqueness arguments, which require strict monotonicity of the functions in (33) and (34).

Formalization scope

Conventions: prices are r : ℕ → ℝ, 1-based, with price r 0 = 0 for $r^{(0)}$; sums over $j = 2, \dots, m$ are over Finset.Icc 2 m. The booking limits are not constructed by Classical.choose: every statement takes functions α, σ together with the hypotheses IsBookingLimits m r α / IsBQLimits m r σ (equations (7)/(8), positivity on $1, \dots, m$, sum $1$). Proposition 1 shows these hypotheses pin down the paper's values on $1, \dots, m$, so no statement is about an arbitrary $\alpha$; a sanity file exhibits solutions for $m = 1$ and for the price set $\{1, 2\}$, so the hypotheses are satisfiable. Standing assumptions are those of the paper: $m \ge 1$ throughout and $m \ge 2$ in Proposition 2, (33), (34), as printed. The constant $1 - 1/e$ is written $1 - e^{-1}$.

Clause (13) is stated for every real root of $1 - e^{-a} = (1-a)/\ln(r^{(m)}/r^{(1)})$; milestone 5 proves that exactly one root exists, so the clause is neither vacuous nor weaker than the printed "the unique solution". The monotonicity of $x/(1 - e^{-x})$ is posed on the printed $[0,1]$ with the value at $0$ set explicitly to the limit $1$, since Lean's $0/0 = 0$ would otherwise give a junk value there.

Everything needed is in Mathlib (Real.exp, Real.log, Real.sqrt, finite sums). Contributions are welcome on any milestone; the monotonicity lemma and Proposition 1 are reusable by the other missions of this series. The paper's proofs are in its Appendix A (pp. 38–39).

Selected references

• W. Ma, D. Simchi-Levi, Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-dependent Competitive Ratios, arXiv:1905.04770v1, 2019; Operations Research 68(6), 2020. https://arxiv.org/abs/1905.04770, https://doi.org/10.1287/opre.2019.1957
• M. O. Ball, M. Queyranne, Toward Robust Revenue Management: Competitive Analysis of Online Booking, Operations Research 57(4), 2009. https://doi.org/10.1287/opre.1080.0654
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990. https://doi.org/10.1145/100216.100262
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and Generalized Online Matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321