Theorem 6: quadratic candidate family with factor two

Proved

ConstrNestedLogit.Space.theorem_6

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

assortment-optimizationknapsacknested-logitp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For a nest with space constraints, there is a single collection $\mathcal A_i$ containing all singleton assortments and rounded optima of the LP relaxation of (10). Every member is feasible, and

|\mathcal A_i|\le(n+1)^2,\qquad \forall u\ge0\ \exists S\in\mathcal A_i:\ \forall T\in C_i,\ V_i(T)(R_i(T)-u)\le2V_i(S)(R_i(S)-u).

This gives an explicit quadratic bound for Theorem 6's $O(n^2)$ collection and supports the overall assortment guarantee through Theorem 4.

Formalization Note Products form a nonempty finite set. The paper's implicit positive preference and space weights are stated explicitly.

Preamble

import Mathlib
import Definitions.Def_ConstrNestedLogit_Space_Model

Formal statement

namespace ConstrNestedLogit.Space

/-- Theorem 6, with the explicit quadratic bound supplied by the line arrangement. -/
theorem theorem_6 {ι : Type*} [Fintype ι] [DecidableEq ι] {n : ℕ}
    (I : NestedLogitVariants.LP.Instance ι n)
    (w : ι → Fin n → ℝ) (c : ι → ℝ) (i : ι)
    (hn : 0 < n)
    (hvnp : ∀ i, I.vnp i = 0) (hv : ∀ j, 0 < I.v i j)
    (hw : ∀ j, 0 < w i j) (hwc : ∀ j, w i j ≤ c i) :
    ∃ A : Finset (Finset (Fin n)),
      isRoundedCandidateFamily I w c i A ∧
      (∀ S ∈ A, spaceFeasible w c i S) ∧
      A.card ≤ (n + 1) ^ 2 ∧
      ∀ u : ℝ, 0 ≤ u → ∃ S ∈ A, isApproximateAt I w c i u 2 S := by sorry

end ConstrNestedLogit.Space

Source

Gallego & Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science (2014), DOI 10.1287/mnsc.2014.1931; authors' manuscript of Sept. 11, 2013, p. 21, Theorem 6

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph