Prove2Me

Theorem 2 (Zhang et al. 2020, Thm 3.1) — the fixed-point framework gives π(x^)≥αz^≥αz∗\pi(\hat x)\ge\alpha\hat z\ge\alpha z^*

Proved
PCLAssort.theorem_2_framework

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

assortment-optimizationlp-roundingmax-dicutp2o-gran-per-chapterp2o-plan-paperp2o-v1paired-combinatorial-logit

Let F\mathcal F be a downward-closed family of assortments containing ∅\emptyset. Suppose that

  1. g:R→Rg:\mathbb R\to\mathbb R satisfies g(z)≥f(z)g(z)\ge f(z) for all z∈Rz\in\mathbb R;
  2. z^≥0\hat z\ge 0 is a fixed point of g(⋅)/v0g(\cdot)/v_0, i.e. g(z^)=v0z^g(\hat z)=v_0\hat z;
  3. x^∈F\hat x\in\mathcal F satisfies ∑(i,j)∈MVij(x^)γij(Rij(x^)−z^)≥α g(z^)\sum_{(i,j)\in M}V_{ij}(\hat x)^{\gamma_{ij}}(R_{ij}(\hat x)-\hat z)\ge\alpha\,g(\hat z) for some α∈[0,1]\alpha\in[0,1].

Then, with z∗z^* the optimal value,

π(x^)≥αz^≥αz∗.\pi(\hat x)\ge\alpha\hat z\ge\alpha z^*.

Thus z^\hat z is an upper bound on z∗z^*, and x^\hat x is an α\alpha-approximate solution: π(x^)≥αz∗\pi(\hat x)\ge\alpha z^*.

Differences from the source:

  • reading: 𝓕 downward closed (p.790) → 𝓕 downward closed and ∅ ∈ 𝓕; reason: every constraint family of the paper contains ∅; with 𝓕 = ∅ the optimal values are undefined
  • reading: v₀ is the no-purchase weight, with no sign stated (p.789) → v₀ > 0 (field of PCLInstance); reason: the paper divides by v₀ (fixed point of g(·)/v₀, p.792); with v₀ = 0 the framework degenerates
  • encoding: γ_ij ∈ [0, 1] (p.789) → γ_ij ∈ (0, 1] for i ≠ j; reason: v_i^{1/γ_ij} is undefined at γ_ij = 0; this excludes only the undefined case
  • encoding: R_ij(x) = 0/0 for an empty nest → Lean's 0/0 = 0; reason: the nest then has weight V_ij(x)^{γ_ij} = 0 (γ_ij > 0), so it contributes nothing either way
Preamble
import Mathlib
import Definitions.Def_PCLAssort_PCLInstance
import Definitions.Def_PCLAssort_DownwardClosed
import Definitions.Def_PCLAssort_revenue
import Definitions.Def_PCLAssort_hz
import Definitions.Def_PCLAssort_optRevenue
import Definitions.Def_PCLAssort_fValue
Formal statement
namespace PCLAssort

/-- Theorem 2 (theorem 3.1 from Zhang et al. 2020) (Ghuge, Kwon, Nagarajan, Sharma, Oper. Res. 70(2), 2022, p.792). Assume an algorithm satisfies
steps 1–3: (1) an upper bound `g(z) ≥ f(z)` for all `z ∈ ℝ`; (2) a fixed point `ẑ ≥ 0` of `g(·)/v_0`,
`g(ẑ) = v_0 ẑ`; (3) an assortment `x̂ ∈ 𝓕` with
`∑_{(i,j)∈M} V_ij(x̂)^{γ_ij} (R_ij(x̂) − ẑ) ≥ α g(ẑ)` for some `α ∈ [0, 1]`. Then
`π(x̂) ≥ α ẑ ≥ α z*`, where `z*` is the optimal value. Thus `ẑ` is an upper bound to the optimal value
and `x̂` is an `α`-approximate solution.

**Formalization Note.** `𝓕` is downward closed and contains `∅` (p.790). The two "thus" sentences
are the conjuncts `z* ≤ ẑ` and `α z* ≤ π(x̂)`. -/
theorem theorem_2_framework {n : ℕ} (I : PCLInstance n) (F : Set (Finset (Fin n)))
    (hF : DownwardClosed F) (g : ℝ → ℝ) (hg : ∀ z, fValue I F z ≤ g z)
    (zhat : ℝ) (hzhat : 0 ≤ zhat) (hfix : g zhat = I.v0 * zhat)
    (xhat : Finset (Fin n)) (hxhat : xhat ∈ F) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α ≤ 1)
    (hstep3 : α * g zhat ≤ hz I zhat xhat) :
    α * zhat ≤ revenue I xhat ∧ α * optRevenue I F ≤ α * zhat ∧
      optRevenue I F ≤ zhat ∧ α * optRevenue I F ≤ revenue I xhat := by sorry

end PCLAssort
Source
Ghuge, Kwon, Nagarajan, Sharma, Constrained Assortment Optimization Under the Paired Combinatorial Logit Model, Oper. Res. 70(2) (2022), Theorem 2, p.792 (PDF p.8)
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph