Lemma 2 — Utility difference rounding bounds
ProvedExponomialAssortment.FPTAS.lemma_2assortment-optimizationexponomialp2o-gran-per-chapterp2o-plan-paperp2o-v1
For every assortment and product i, the rounded utility difference sum lies between the exact sum minus iδ and the exact sum plus iδ, where δ=η/(2n) and source indices start at one.
Differences from the source:
- encoding: one-based indicators and normalized utilities → Fin n, finite selected sets, Valid and Feasible with 1 ≤ C ≤ n; reason: equivalent indexing and the cardinality extension explicitly asserted in §8, counting the outside option; C=n recovers the unconstrained setting
Preamble
import Definitions.Def_ExponomialAssortment_FPTAS_Rounding
Formal statement
namespace ExponomialAssortment.FPTAS
theorem lemma_2 (n : ℕ) (I : Instance n) (hI : Valid I) (C : ℕ)
(hC : 1 ≤ C ∧ C ≤ n) (η : ℝ) (hη : 0 < η)
(S : Finset (Fin n)) (hS : Feasible I C S) (i : Fin n) :
gapSum I.utility S i - (i.val + 1) * delta n η ≤ gapSum (roundedUtility I η) S i ∧
gapSum (roundedUtility I η) S i ≤ gapSum I.utility S i + (i.val + 1) * delta n η := by sorry
end ExponomialAssortment.FPTAS
Source
Aouad, Feldman and Segev (2023), DOI 10.1287/mnsc.2022.4492, published repository manuscript, Lemma 2, printed p. 17, PDF p. 18
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.