Prove2Me

Claim G.1 — δ\delta is unimodal with maximum at a(S1)a(S2)\sqrt{a(S_1)a(S_2)} and symmetric under y↦a(S1)a(S2)/yy\mapsto a(S_1)a(S_2)/y

Proved
SponsoredAssort.claim_G_1

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

assortment-optimizationcompetitive-ratiomechanism-designmnl-choice-modelp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1

Fix a seller ii with ri>0r_i>0 and the others' attractiveness v−iv_{-i}, and write a(S)=1+∑j∈S∖{i}vja(S)=1+\sum_{j\in S\setminus\{i\}}v_j. Let S1,S2S_1,S_2 be assortments with i∈S1i\in S_1, i∈S2i\in S_2 and a(S1)<a(S2)a(S_1)<a(S_2), and define δ:R+→R\delta:\mathbb R_+\to\mathbb R by

δ(y)=ri πi(S1,(y,v−i))−ri πi(S2,(y,v−i)).\delta(y)=r_i\,\pi_i\big(S_1,(y,v_{-i})\big)-r_i\,\pi_i\big(S_2,(y,v_{-i})\big).

Then δ\delta is unimodal with its maximum at c=a(S1)a(S2)c=\sqrt{a(S_1)a(S_2)}:

  1. δ\delta is strictly increasing on [0,c][0,c];
  2. δ\delta is strictly decreasing on [c,∞)[c,\infty);
  3. δ(y)=δ(a(S1)a(S2)/y)\delta(y)=\delta\big(a(S_1)a(S_2)/y\big) for every y>0y>0.

The claim compares two assortments containing seller ii as seller ii's attractiveness varies, and drives Corollary 5.1.

Differences from the source:

  • encoding: unimodal (increasing and then decreasing) with a maximum at a(S1)a(S2)\sqrt{a(S_1)a(S_2)} → strictly increasing on [0,c][0,c] and strictly decreasing on [c,∞)[c,\infty); reason: this is the meaning of unimodality with maximum at cc
  • encoding: δ(y)=δ(a(S1)a(S2)/y)\delta(y)=\delta(a(S_1)a(S_2)/y) for all yy → for all y>0y>0; reason: a(S1)a(S2)/ya(S_1)a(S_2)/y is undefined at y=0y=0
  • generalization: standing revenues r1≥⋯≥rn>0r_1\ge\dots\ge r_n>0 → only ri>0r_i>0; reason: the claim involves only rir_i; it specializes to the standing setting
Preamble
import Mathlib
import Definitions.Def_SponsoredAssort_choiceProb
import Definitions.Def_SponsoredAssort_others

open scoped NNReal
Formal statement
namespace SponsoredAssort

/-- **Claim G.1** (Balseiro, Désir, SSRN 3821382 (Feb. 21, 2022), Appendix G.1, OA p.36). Fix a
seller `i` with `rᵢ > 0` and `v₋ᵢ`, and write `a(S) = 1 + ∑_{j ∈ S \ {i}} vⱼ`. For assortments
`S₁, S₂` with `i ∈ S₁`, `i ∈ S₂` and `a(S₁) < a(S₂)`, the function
`δ(y) = rᵢ · πᵢ(S₁, (y, v₋ᵢ)) − rᵢ · πᵢ(S₂, (y, v₋ᵢ))` on `ℝ₊` is unimodal with maximum at
`√(a(S₁)a(S₂))`: strictly increasing on `[0, √(a(S₁)a(S₂))]` and strictly decreasing on
`[√(a(S₁)a(S₂)), ∞)`. Moreover `δ(y) = δ(a(S₁)a(S₂)/y)`.

**Formalization Note.** "Unimodal (increasing and then decreasing) with a maximum at `√(a₁a₂)`" is
stated as strict monotonicity on each side of `√(a₁a₂)`. The symmetry is stated for `y > 0`,
where `a₁a₂/y` is defined; `a₁a₂/y ≥ 0`, so `Real.toNNReal` is exact. `rᵢ > 0` is the paper's
standing assumption (p.9). -/
theorem claim_G_1 {n : ℕ} (r : Fin n → ℝ) (v : Attr n) (i : Fin n) (hr : 0 < r i)
    (S₁ S₂ : Finset (Fin n)) (h₁ : i ∈ S₁) (h₂ : i ∈ S₂) (ha : others v i S₁ < others v i S₂) :
    let δ : ℝ≥0 → ℝ := fun y =>
      r i * choiceProb S₁ (Function.update v i y) i - r i * choiceProb S₂ (Function.update v i y) i
    (∀ y z : ℝ≥0, y < z → (z : ℝ) ≤ Real.sqrt (others v i S₁ * others v i S₂) → δ y < δ z) ∧
    (∀ y z : ℝ≥0, Real.sqrt (others v i S₁ * others v i S₂) ≤ (y : ℝ) → y < z → δ z < δ y) ∧
    (∀ y : ℝ≥0, 0 < y →
      δ y = δ (Real.toNNReal (others v i S₁ * others v i S₂ / (y : ℝ)))) := by sorry

end SponsoredAssort
Source
Balseiro, Désir, Incentive-Compatible Assortment Optimization for Sponsored Products, SSRN 3821382 (Feb. 21, 2022), Appendix G.1, Claim G.1, OA p.36
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