Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Collections

Revenue Management and Choice Models

Dynamic pricing, assortment optimization, discrete choice models, and airline seat control.

23 completed missions

Missions

21–23 of 23
OpenCompletedAll
🏆Completed
Convex OptimizationLinear OptimizationStatistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 4: Existence of the Maximum Likelihood Estimate Is Decided by a Quadratic ProgramResearch Paper

Why a likelihood maximum needs a diagnostic

The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.

The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.

Choice experiments and weighted differences

There are N≥1N\geq1N≥1 trials. Trial nnn offers JnJ_nJn​ alternatives, indexed by iii and jjj. Alternative iii has an attribute vector zin∈RKz_{in}\in\mathbb R^Kzin​∈RK, and SinS_{in}Sin​ counts how many times it was selected in that trial. Each trial has at least two alternatives and Rn=∑iSin>0R_n=\sum_iS_{in}>0Rn​=∑i​Sin​>0 observations. The vector θ∈RK\theta\in\mathbb R^Kθ∈RK is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative iii a probability proportional to exp⁡(zin⋅θ)\exp(z_{in}\cdot\theta)exp(zin​⋅θ), with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).

For the test, define the weighted difference

wnij=Sin(zjn−zin)∈RK.w_{nij}=S_{in}(z_{jn}-z_{in})\in\mathbb R^K.wnij​=Sin​(zjn​−zin​)∈RK.

It is indexed by every trial and every ordered pair of alternatives, including i=ji=ji=j and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.

Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank KKK. Equivalently, the vectors zjn−zinz_{jn}-z_{in}zjn​−zin​ span RK\mathbb R^KRK; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction γ∈RK\gamma\in\mathbb R^Kγ∈RK satisfies wnij⋅γ≤0w_{nij}\cdot\gamma\leq0wnij​⋅γ≤0 for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.

Formalization targets

Lemma 4: a quadratic-programming test

Let QQQ be the set of feasible vectors

Q={y=∑n=1N∑i,j=1Jnαijnwnij:αijn≥1 for all n,i,j}.Q=\left\{y=\sum_{n=1}^{N}\sum_{i,j=1}^{J_n}\alpha_{ijn}w_{nij}: \alpha_{ijn}\geq1\text{ for all }n,i,j\right\}.Q={y=n=1∑N​i,j=1∑Jn​​αijn​wnij​:αijn​≥1 for all n,i,j}.

The mission's goal is the equivalence in Lemma 4:

Axiom 6 holds⟺min⁡y∈Qy⋅y=0.\text{Axiom 6 holds} \quad\Longleftrightarrow\quad \min_{y\in Q}y\cdot y=0.Axiom 6 holds⟺y∈Qmin​y⋅y=0.

The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the wnijw_{nij}wnij​ gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).

What the result provides

Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.

The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.

Why the equivalence is delicate

The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints αijn≥1\alpha_{ijn}\geq1αijn​≥1 in equation (22). Both conditions must appear in their proper places.

The full-rank condition alone does not ensure that the vectors wnijw_{nij}wnij​ span the attribute space if a trial has no observed choices. The section describes RnR_nRn​ repetitions of each trial, and the formal data require Rn>0R_n>0Rn​>0. This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.

Formalization scope

Lean represents a nonempty set of trials by Fin N, alternatives in trial nnn by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count RnR_nRn​ is the sum of observed choice counts. The model requires Jn≥2J_n\geq2Jn​≥2 and Rn>0R_n>0Rn​>0 for each trial. There is no extra assumption that K>0K>0K>0: the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.

Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every n,i,jn,i,jn,i,j from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.

The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.

Selected references

  • Daniel McFadden, “Conditional Logit Analysis of Qualitative Choice Behavior,” in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142; especially pp. 113–117, Axioms 5–6, Lemmas 3–4, and equation (22). Book catalog search.
5 thms2 active usersReviewed
🏆Completed
Convex OptimizationOperations ResearchStatistics·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≥1N \ge 1N≥1 trials. Trial nnn offers an alternative set of JnJ_nJn​ alternatives, indexed i=1,…,Jni = 1,\dots,J_ni=1,…,Jn​, each described by an attribute vector zin∈RKz_{in} \in \mathbb{R}^Kzin​∈RK (the values of KKK specified functions of the individual's and the alternative's characteristics). Trial nnn is repeated Rn≥1R_n \ge 1Rn​≥1 times, and alternative iii is chosen SinS_{in}Sin​ times, so Rn=∑jSjnR_n = \sum_{j} S_{jn}Rn​=∑j​Sjn​.

For a parameter θ∈RK\theta \in \mathbb{R}^Kθ∈RK, with zinθz_{in}\thetazin​θ the inner product, the selection probabilities are

Pin(θ)=ezinθ∑j=1Jnezjnθ(16)P_{in}(\theta) = \frac{e^{z_{in}\theta}}{\sum_{j=1}^{J_n} e^{z_{jn}\theta}} \qquad (16)Pin​(θ)=∑j=1Jn​​ezjn​θezin​θ​(16)

and the log-likelihood of the sample is

L(θ)=C−∑n=1N∑i=1JnSinlog⁡∑j=1Jne(zjn−zin)θ,C=∑n=1N[log⁡Rn!−∑j=1Jnlog⁡Sjn!].(18)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)L(θ)=C−n=1∑N​i=1∑Jn​​Sin​logj=1∑Jn​​e(zjn​−zin​)θ,C=n=1∑N​[logRn​!−j=1∑Jn​​logSjn​!].(18)

Write zˉn(θ)=∑izinPin(θ)\bar z_n(\theta) = \sum_i z_{in}P_{in}(\theta)zˉn​(θ)=∑i​zin​Pin​(θ) for the probability-weighted mean attribute vector of trial nnn.

Axiom 5 (Full Rank). The (∑nJn)×K\big(\sum_n J_n\big)\times K(∑n​Jn​)×K matrix with rows zin−zˉnz_{in} - \bar z_nzin​−zˉn​ has rank KKK.

Axiom 6. There is no nonzero γ∈RK\gamma \in \mathbb{R}^Kγ∈RK with Sin(zjn−zin)γ≤0S_{in}(z_{jn} - z_{in})\gamma \le 0Sin​(zjn​−zin​)γ≤0 for all i,j=1,…,Jni, j = 1,\dots,J_ni,j=1,…,Jn​ and n=1,…,Nn = 1,\dots,Nn=1,…,N. Equivalently, no nonzero direction makes every observed choice weakly best in its alternative set.

Formalization targets

Goal: Lemma 3

Under Axiom 5,

(∃ θ^∈RK, ∀θ, L(θ)≤L(θ^))  ⟺  Axiom 6.\big(\exists\, \hat\theta \in \mathbb{R}^K,\ \forall \theta,\ L(\theta) \le L(\hat\theta)\big) \iff \text{Axiom 6}.(∃θ^∈RK, ∀θ, L(θ)≤L(θ^))⟺Axiom 6.

Milestones

  1. Equation (19): the gradient ∂L/∂θ=∑n∑j(Sjn−RnPjn)zjn\partial L/\partial\theta = \sum_n \sum_j (S_{jn} - R_nP_{jn}) z_{jn}∂L/∂θ=∑n​∑j​(Sjn​−Rn​Pjn​)zjn​.
  2. Equation (20): the Hessian ∂2L/∂θ ∂θ′=−∑nRn∑j(zjn−zˉn)′Pjn(zjn−zˉn)\partial^2L/\partial\theta\,\partial\theta' = -\sum_n R_n \sum_j (z_{jn} - \bar z_n)'P_{jn}(z_{jn} - \bar z_n)∂2L/∂θ∂θ′=−∑n​Rn​∑j​(zjn​−zˉn​)′Pjn​(zjn​−zˉn​).
  3. LLL is concave, and every critical point is a global maximizer.
  4. A Hessian that is nonsingular everywhere makes LLL strictly concave with at most one maximizer.
  5. Axiom 5 holds at θ\thetaθ if and only if the Hessian at θ\thetaθ is negative definite.
  6. Necessity: under Axiom 5, a maximizer forces Axiom 6.
  7. Equation (21): under Axiom 6, b(γ)=max⁡nmax⁡i,jSin(zjn−zin)γb(\gamma) = \max_n \max_{i,j} S_{in}(z_{jn}-z_{in})\gammab(γ)=maxn​maxi,j​Sin​(zjn​−zin​)γ has a positive lower bound b∗b^*b∗ on the unit sphere.
  8. The bound L(θ)−C≤−b∗∣θ∣L(\theta) - C \le -b^*|\theta|L(θ)−C≤−b∗∣θ∣ for all θ\thetaθ.
  9. 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 RK\mathbb{R}^KRK 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 CCC, hence attains its maximum", fails: LLL is bounded but can approach its supremum only at infinity, which is exactly the separation case. Sufficiency needs a quantitative rate at which LLL 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 Rn=0R_n = 0Rn​=0 can supply the rank of Axiom 5 while contributing nothing to LLL, 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. RK\mathbb{R}^KRK is EuclideanSpace ℝ (Fin K), so ∣θ∣=(θ′θ)1/2|\theta| = (\theta'\theta)^{1/2}∣θ∣=(θ′θ)1/2 is the Euclidean norm and zθz\thetazθ is the inner product ⟪z, θ⟫. Trials are Fin N, alternatives of trial nnn are Fin (J n), and the counts SinS_{in}Sin​ are natural numbers.
  • Data structure. The structure Data K bundles NNN, JJJ, zzz, SSS and the standing assumptions N≥1N \ge 1N≥1 and Rn=∑iSin≥1R_n = \sum_i S_{in} \ge 1Rn​=∑i​Sin​≥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 vvv 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 RK\mathbb{R}^KRK. Neither a local maximizer nor "L(θ^)≥L(0)L(\hat\theta) \ge L(0)L(θ^)≥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
Linear OptimizationOperations ResearchOptimization·Captain: mikedeng1

Assortment Optimization under Variants of the Nested Logit Model 1: If the Restricted LP Optimum Scaled by α Is Feasible for the Full LP, Its Assortment Earns Within a Factor α of the Optimal RevenueResearch Paper

Motivation

A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.

Setting

There are mmm nests MMM and nnn products N={1,…,n}N = \{1, \dots, n\}N={1,…,n} in each nest. Product jjj of nest iii has revenue rij≥0r_{ij} \ge 0rij​≥0 and preference weight vij>0v_{ij} > 0vij​>0, and the products in each nest are ordered so that ri1≥⋯≥rinr_{i1} \ge \dots \ge r_{in}ri1​≥⋯≥rin​. Nest iii has a no-purchase weight vi0≥0v_{i0} \ge 0vi0​≥0 and a dissimilarity parameter γi>0\gamma_i > 0γi​>0. The weight of choosing no nest at all is v0≥0v_0 \ge 0v0​≥0. If the assortment Si⊆NS_i \subseteq NSi​⊆N is offered in nest iii, write

Vi(Si)=vi0+∑j∈Sivij,Ri(Si)=∑j∈SirijvijVi(Si),Ri(∅)=0.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 .Vi​(Si​)=vi0​+j∈Si​∑​vij​,Ri​(Si​)=Vi​(Si​)∑j∈Si​​rij​vij​​,Ri​(∅)=0.

A customer picks nest iii with probability Qi=Vi(Si)γi/(v0+∑l∈MVl(Sl)γl)Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l\in M} V_l(S_l)^{\gamma_l})Qi​=Vi​(Si​)γi​/(v0​+∑l∈M​Vl​(Sl​)γl​), and then a product of that nest by the multinomial logit model. The expected revenue is

Π(S1,…,Sm)=∑i∈MQi(S1,…,Sm) Ri(Si),\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i(S_1, \dots, S_m)\, R_i(S_i),Π(S1​,…,Sm​)=i∈M∑​Qi​(S1​,…,Sm​)Ri​(Si​),

and problem (2) is Z∗=max⁡Si⊆NΠ(S1,…,Sm)Z^* = \max_{S_i \subseteq N} \Pi(S_1, \dots, S_m)Z∗=maxSi​⊆N​Π(S1​,…,Sm​).

The linear program (3) in the variables (x,y1,…,ym)(x, y_1, \dots, y_m)(x,y1​,…,ym​) minimizes xxx subject to

v0x≥∑i∈Myi,yi≥Vi(Si)γi(Ri(Si)−x)∀Si⊆N, i∈M.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) \quad \forall S_i \subseteq N,\ i \in M.v0​x≥i∈M∑​yi​,yi​≥Vi​(Si​)γi​(Ri​(Si​)−x)∀Si​⊆N, i∈M.

Given candidate collections {Ait:t∈Ti}\{A_{it} : t \in \mathcal T_i\}{Ait​:t∈Ti​} of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for SiS_iSi​ in the collection of nest iii.

Formalization targets

Goal: Theorem 1 (p. 13)

Let (x^,y^)(\hat x, \hat y)(x^,y^​) be an optimal solution of (4), and let S^i\hat S_iS^i​ solve max⁡Si∈{Ait}Vi(Si)γi(Ri(Si)−x^)\max_{S_i \in \{A_{it}\}} V_i(S_i)^{\gamma_i}(R_i(S_i) - \hat x)maxSi​∈{Ait​}​Vi​(Si​)γi​(Ri​(Si​)−x^), problem (5), in every nest. If (αx^,βy^)(\alpha \hat x, \beta \hat y)(αx^,βy^​) is feasible for (3) for some α,β\alpha, \betaα,β, then, with Z^=Π(S^1,…,S^m)\hat Z = \Pi(\hat S_1, \dots, \hat S_m)Z^=Π(S^1​,…,S^m​),

αZ^ ≥ Z∗ ≥ Z^.\alpha \hat Z \ \ge\ Z^* \ \ge\ \hat Z .αZ^ ≥ Z∗ ≥ Z^.

The theorem fixes no candidate collection and no value of α\alphaα. Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.

Milestones (§2, pp. 11–12)

  1. Problem (2) is equivalent to (3): Z∗Z^*Z∗ is the least xxx for which some yyy makes (x,y)(x, y)(x,y) feasible for (3).
  2. At an optimal solution of (4), the first constraint binds at the maximizers S^i\hat S_iS^i​ of (5), and x^=Π(S^1,…,S^m)\hat x = \Pi(\hat S_1, \dots, \hat S_m)x^=Π(S^1​,…,S^m​).
  3. Problem (4) relaxes (3), so x^≤Z∗\hat x \le Z^*x^≤Z∗.

Companions (§7, pp. 29–30)

  • The tighter program (16), which lets each nest's assortment be a fractional vector zi∈[0,1]nz_i \in [0,1]^nzi​∈[0,1]n, has every feasible xxx above Z∗Z^*Z∗.
  • Proposition 13: F^i(x)=max⁡zi∈[0,1]nFi(zi∣x)\hat F_i(x) = \max_{z_i \in [0,1]^n} F_i(z_i \mid x)F^i​(x)=maxzi​∈[0,1]n​Fi​(zi​∣x) is convex, with subgradient −(vi0+∑jvijz^ij(x))γi-(v_{i0} + \sum_j v_{ij}\hat z_{ij}(x))^{\gamma_i}−(vi0​+∑j​vij​z^ij​(x))γi​ at xxx.

Significance

Theorem 1 is the common step behind the paper's four approximation guarantees: the factor ρ\rhoρ or 2κ2\kappa2κ of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the δ2γˉ+1\delta^{2\bar\gamma+1}δ2γˉ​+1 of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, v0=0v_0 = 0v0​=0), and a formal proof certifies the framework once for every later instantiation.

Difficulty

The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective Π≤x\Pi \le xΠ≤x as a linear constraint. Both steps need care where a denominator v0+∑iVi(Si)γiv_0 + \sum_i V_i(S_i)^{\gamma_i}v0​+∑i​Vi​(Si​)γi​ can vanish. The binding argument for (4) is a perturbation argument: lowering x^\hat xx^ must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in xxx. The obvious one-line reading of Theorem 1, "x^=Z^\hat x = \hat Zx^=Z^ and αx^≥Z∗\alpha\hat x \ge Z^*αx^≥Z∗", is correct only once both of these facts are established with their hypotheses. In particular, it is false when v0=0v_0 = 0v0​=0 (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of FiF_iFi​ on [0,1]n[0,1]^n[0,1]n.

Formalization scope

Nests are a finite type ι and products are Fin n, indexed 0,…,n−10, \dots, n-10,…,n−1. An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's x/0=0x / 0 = 0x/0=0 gives Ri(∅)=0R_i(\emptyset) = 0Ri​(∅)=0. Z∗Z^*Z∗ is Π(S∗)\Pi(S^*)Π(S∗) for an arbitrary optimal assortment S∗S^*S∗; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal xxx, and "S^i\hat S_iS^i​ solves (5)" means S^i\hat S_iS^i​ belongs to the collection of nest iii and maximizes the objective of (5) over it at x^\hat xx^.

Standing assumptions and pins. These are v0,vi0≥0v_0, v_{i0} \ge 0v0​,vi0​≥0 and ordered revenues, together with vij>0v_{ij} > 0vij​>0, rij≥0r_{ij} \ge 0rij​≥0 and γi>0\gamma_i > 0γi​>0. The paper allows zero-weight padding products and γi=0\gamma_i = 0γi​=0, but its own conventions fail there. Theorem 1 and the binding milestone add v0>0v_0 > 0v0​>0. The page allows v0=0v_0 = 0v0​=0, but then Theorem 1 is false: take one nest with v10=0v_{10} = 0v10​=0, γ1=1\gamma_1 = 1γ1​=1, r11=v11=1r_{11} = v_{11} = 1r11​=v11​=1 and candidates {∅,{1}}\{\emptyset, \{1\}\}{∅,{1}}. Then x^=1\hat x = 1x^=1 and S^1=∅\hat S_1 = \emptysetS^1​=∅ meet every hypothesis with α=β=1\alpha = \beta = 1α=β=1, yet Z^=0<Z∗=1\hat Z = 0 < Z^* = 1Z^=0<Z∗=1. The equivalence of (2) and (3) and the bound from (16) keep v0≥0v_0 \ge 0v0​≥0, as the page does, and assume at least one nest and one product: with neither and v0=0v_0 = 0v0​=0, every xxx is feasible for (3).

A formalization that assumes the binding equality, the identity x^=Z^\hat x = \hat Zx^=Z^, or the inequality x^≤Z∗\hat x \le Z^*x^≤Z∗ in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.

The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.

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). https://doi.org/10.1287/opre.2014.1256
  • D. McFadden, Econometric models of probabilistic choice, in C. Manski, D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981. https://eml.berkeley.edu/~mcfadden/discrete.html
  • P. Rusmevichientong, D. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, Technical report, Cornell University, 2010. https://people.orie.cornell.edu/huseyin/publications/publications.html
  • M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993. https://doi.org/10.1002/0471787779
6 thms2 active usersReviewed
Previous

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me