Prove2Me

Example 1(a), seller half — the seller's strategy is a best response

Proved
ChatterjeeSamuelson.UniformEquilibrium.seller_best_response

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

bargaininggame-theoryincomplete-informationp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let 0≤k≤10 \le k \le 1 and vˉ>0\bar v > 0, let both reservation prices lie in [0,vˉ][0, \bar v], and let each player's belief about the other's value be uniform on [0,vˉ][0, \bar v]. Let S,B:R→RS, B : \mathbb R \to \mathbb R be measurable offer strategies such that

  1. S(vs)=vs2−k+1−k2vˉS(v_s) = \frac{v_s}{2-k} + \frac{1-k}{2}\bar v for 0≤vs≤2−k2vˉ0 \le v_s \le \frac{2-k}{2}\bar v;
  2. S(vs)≥vs2−k+1−k2vˉS(v_s) \ge \frac{v_s}{2-k} + \frac{1-k}{2}\bar v for 2−k2vˉ<vs≤vˉ\frac{2-k}{2}\bar v < v_s \le \bar v;
  3. B(vb)≤vb1+k+k(1−k)2(1+k)vˉB(v_b) \le \frac{v_b}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v for 0≤vb<1−k2vˉ0 \le v_b < \frac{1-k}{2}\bar v;
  4. B(vb)=vb1+k+k(1−k)2(1+k)vˉB(v_b) = \frac{v_b}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v for 1−k2vˉ≤vb≤vˉ\frac{1-k}{2}\bar v \le v_b \le \bar v.

Then for every seller value v∈[0,vˉ]v \in [0, \bar v] and every real ask ss,

πs(s,v)≤πs(S(v),v),\pi_s(s, v) \le \pi_s(S(v), v),

where πs\pi_s is the seller's expected profit against BB under the uniform belief. That is, SS is a best response to BB for every seller type.

Together with the buyer half, this is the statement that (S,B)(S, B) is an equilibrium (Example 1(a)).

Formalization Note Measurability of SS and BB is added: the page leaves SS on the upper range and BB on the lower range free up to an inequality, and a non-measurable choice would make expected profits meaningless. The printed coefficient (k(1−k)/2(1+k))vˉ(k(1-k)/2(1+k))\bar v is read as k(1−k)2(1+k)vˉ\frac{k(1-k)}{2(1+k)}\bar v.

Preamble
import Mathlib
import Definitions.Def_ChatterjeeSamuelson_Shared_unif
import Definitions.Def_ChatterjeeSamuelson_Shared_buyerProfit
import Definitions.Def_ChatterjeeSamuelson_Shared_sellerProfit
import Definitions.Def_ChatterjeeSamuelson_Shared_sellerLinear
import Definitions.Def_ChatterjeeSamuelson_Shared_buyerLinear

open MeasureTheory ProbabilityTheory Set
Formal statement
namespace ChatterjeeSamuelson.UniformEquilibrium

/-- Example 1(a), seller half (Chatterjee & Samuelson, *Bargaining under Incomplete
Information*, Oper. Res. 31(5) 1983, §3, Example 1(a), p. 842 [PDF 8]): with both values
uniform on `[0, v̄]` (`F_s(v) = F_b(v) = v/v̄`), the seller's strategy `S` of Example 1(a) is a
best response to the buyer's strategy `B` of Example 1(a): for every seller value
`v ∈ [0, v̄]` and every real ask `s`, `π_s(s, v) ≤ π_s(S(v), v)`, where the seller's belief
about the buyer's value is uniform on `[0, v̄]`.

Hypotheses: `0 ≤ k ≤ 1`, `0 < v̄`, `S` and `B` measurable, and the four lines of
Example 1(a) on their printed ranges:
1. `S v = v/(2 − k) + ((1 − k)/2) v̄` for `0 ≤ v ≤ ((2 − k)/2) v̄`;
2. `S v ≥ v/(2 − k) + ((1 − k)/2) v̄` for `((2 − k)/2) v̄ < v ≤ v̄`;
3. `B v ≤ v/(1 + k) + (k(1 − k)/(2(1 + k))) v̄` for `0 ≤ v < ((1 − k)/2) v̄`;
4. `B v = v/(1 + k) + (k(1 − k)/(2(1 + k))) v̄` for `((1 − k)/2) v̄ ≤ v ≤ v̄`.
`S`, `B` are unconstrained outside `[0, v̄]`.

*Formalization Note.*
`Measurable S`, `Measurable B` are added: the page leaves `S` above
`((2 − k)/2) v̄` and `B` below `((1 − k)/2) v̄` free up to an inequality, and a
non-measurable choice would make an expected profit a junk Bochner integral; the paper's
offer densities `g_b`, `g_s` presuppose measurable strategies. The printed coefficient `k(1 − k)/2(1 + k)` is read as
`k(1 − k)/(2(1 + k))` (see `buyerLinear`). -/
theorem seller_best_response (k vbar : ℝ) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hvbar : 0 < vbar)
    (S B : ℝ → ℝ) (hSmeas : Measurable S) (hBmeas : Measurable B)
    (hS_eq : ∀ v, 0 ≤ v → v ≤ (2 - k) / 2 * vbar → S v = Shared.sellerLinear k vbar v)
    (hS_ge : ∀ v, (2 - k) / 2 * vbar < v → v ≤ vbar → Shared.sellerLinear k vbar v ≤ S v)
    (hB_le : ∀ v, 0 ≤ v → v < (1 - k) / 2 * vbar → B v ≤ Shared.buyerLinear k vbar v)
    (hB_eq : ∀ v, (1 - k) / 2 * vbar ≤ v → v ≤ vbar → B v = Shared.buyerLinear k vbar v) :
    ∀ v ∈ Icc (0 : ℝ) vbar, ∀ s : ℝ,
      Shared.sellerProfit k (Shared.unif vbar) B s v ≤ Shared.sellerProfit k (Shared.unif vbar) B (S v) v := by sorry

end ChatterjeeSamuelson.UniformEquilibrium
Source
Chatterjee & Samuelson, Bargaining under Incomplete Information, Oper. Res. 31(5) (1983), https://doi.org/10.1287/opre.31.5.835, p. 842 [PDF 8], Example 1(a) (seller's best-response half)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

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

View graph