Theorem 4.2 — Augmented Greedy recovers a fraction of complete-type revenue
ProvedCustAssort.AugGreedy.theorem_4_2Consider CAP with positive product revenues ordered from highest to lowest, nonnegative MNL preference weights, and nonnegative type-arrival probabilities summing to one. Let be an optimal first-stage assortment under capacity . For customer types , products , and any , let be any output of Augmented Greedy on . A type is complete with respect to when every product of belongs to its threshold optimal personalized assortment. Write for the complete types in . Then
This structural bound is the paper's guarantee for Augmented Greedy and a building block for its later CAP approximation results.
Formalization Note The theorem covers every legal Greedy run and every tie-breaking choice of Augmented Greedy. The threshold optimal assortment is , as in Lemma E.1. is independent of .
import Mathlib import Definitions.Def_CustAssort_AugGreedy_Setting
namespace CustAssort.AugGreedy
/-- Theorem 4.2, p. 11: Augmented Greedy captures a 1−1/e fraction of complete-type revenue. -/
theorem theorem_4_2 {n m : ℕ} (θ : Fin m → ℝ) (v : Fin n → Fin m → ℝ)
(r : Fin n → ℝ) (hr : ∀ i, 0 < r i) (hv : ∀ i j, 0 ≤ v i j)
(hθ : ∀ j, 0 ≤ θ j) (hθsum : ∑ j, θ j = 1) (hanti : Antitone r)
(K : ℕ) (Sstar : Finset (Fin n)) (hS : IsCAPOpt θ v r K Sstar)
(C : Finset (Fin m)) (P : Finset (Fin n)) (k : ℕ)
(hk : (P ∩ Sstar).card ≤ k) (Δ : Finset (Fin n))
(hΔ : IsAugGreedyOutput θ v r C k Δ) :
(1 - Real.exp (-1)) *
fC θ v r (completeTypes v r Sstar C P) (P ∩ Sstar) ≤ fC θ v r C Δ := by sorry
end CustAssort.AugGreedy
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.