Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 1 — the unique pricing equilibrium is linear in the demand signal (production economy)

Proved
InfoSharing.Economy.lemma_1_pricing_equilibrium

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

bayesian-gameinformation-sharingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain

Let ϕ>0\phi > 0ϕ>0 and 0<ce<2/(1+ϕ)0 < c_e < 2/(1+\phi)0<ce​<2/(1+ϕ), put c=−cec = -c_ec=−ce​, and let a,ba, ba,b be reals. Let (θ,Y)(\theta, Y)(θ,Y) satisfy the signal model with variance σ2\sigma^2σ2 and weight β=β(t,σ)\beta = \beta(t,\sigma)β=β(t,σ). For every status profile XXX the pricing game of §4.1 has an equilibrium, and, provided ce≠ce∗c_e \ne c_e^*ce​=ce∗​ (see the note), in every equilibrium (ρ,f)(\rho, f)(ρ,f), for each manufacturer iii, almost surely

wi∗=fi(Y)=wˉ+αw Y,pi∗=ρ(w∗,Y)i=pˉ+αp Y,w_i^* = f_i(Y) = \bar w + \alpha_w\,Y, \qquad p_i^* = \rho(w^*, Y)_i = \bar p + \alpha_p\,Y,wi∗​=fi​(Y)=wˉ+αw​Y,pi∗​=ρ(w∗,Y)i​=pˉ​+αp​Y,

where wˉ=(1+(1+ϕ)c)a+(1+ϕ)b2+ϕ+(1+ϕ)c\bar w = \frac{(1+(1+\phi)c)a + (1+\phi)b}{2+\phi+(1+\phi)c}wˉ=2+ϕ+(1+ϕ)c(1+(1+ϕ)c)a+(1+ϕ)b​, pˉ=(3+ϕ+2(1+ϕ)c)a+(1+ϕ)b2(2+ϕ+(1+ϕ)c)\bar p = \frac{(3+\phi+2(1+\phi)c)a + (1+\phi)b}{2(2+\phi+(1+\phi)c)}pˉ​=2(2+ϕ+(1+ϕ)c)(3+ϕ+2(1+ϕ)c)a+(1+ϕ)b​, and αw\alpha_wαw​, αp\alpha_pαp​ are the coefficients of Lemma 1 selected by nnn and, when n=1n = 1n=1, by XiX_iXi​:

  1. αw(0)=αwU(1)=0\alpha_w(0) = \alpha_w^U(1) = 0αw​(0)=αwU​(1)=0, αwI(1)=1+(1+ϕ)c(1+ϕ)(2+(1+ϕ)c)β\alpha_w^I(1) = \frac{1+(1+\phi)c}{(1+\phi)(2+(1+\phi)c)}\betaαwI​(1)=(1+ϕ)(2+(1+ϕ)c)1+(1+ϕ)c​β, αw(2)=1+(1+ϕ)c2+ϕ+(1+ϕ)cβ\alpha_w(2) = \frac{1+(1+\phi)c}{2+\phi+(1+\phi)c}\betaαw​(2)=2+ϕ+(1+ϕ)c1+(1+ϕ)c​β;
  2. αp(0)=αpU(1)=β2\alpha_p(0) = \alpha_p^U(1) = \frac{\beta}{2}αp​(0)=αpU​(1)=2β​, αpI(1)=3+2ϕ+(1+ϕ)(2+ϕ)c2(1+ϕ)(2+(1+ϕ)c)β\alpha_p^I(1) = \frac{3+2\phi+(1+\phi)(2+\phi)c}{2(1+\phi)(2+(1+\phi)c)}\betaαpI​(1)=2(1+ϕ)(2+(1+ϕ)c)3+2ϕ+(1+ϕ)(2+ϕ)c​β, αp(2)=3+ϕ+2(1+ϕ)c2(2+ϕ+(1+ϕ)c)β\alpha_p(2) = \frac{3+\phi+2(1+\phi)c}{2(2+\phi+(1+\phi)c)}\betaαp​(2)=2(2+ϕ+(1+ϕ)c)3+ϕ+2(1+ϕ)c​β.

An informed manufacturer's wholesale price responds to the signal, positively when ce<1/(1+ϕ)c_e < 1/(1+\phi)ce​<1/(1+ϕ) and negatively when ce>1/(1+ϕ)c_e > 1/(1+\phi)ce​>1/(1+ϕ); an uninformed one's does not. All ex ante profits of §4.2 follow from this equilibrium.

Formalization Note The production economy model takes c=−cec = -c_ec=−ce​ with 0<ce<2/(1+ϕ)0 < c_e < 2/(1+\phi)0<ce​<2/(1+ϕ) (the Assumption of p. 251). The ex ante profits are those of an equilibrium of the pricing game on the signal model, not the closed forms: the closed forms are the content of the §4.2 milestones. The production cost is the uncapped quadratic bq−ceq2bq - c_e q^2bq−ce​q2 (the paper's cap at qˉ=b/(2ce)\bar q = b/(2c_e)qˉ​=b/(2ce​) is assumed never to bind, footnote 11, p. 251). Correction of the paper. Uniqueness is asserted only for ce≠c_e \nece​= ce∗=2+3ϕ(1+2ϕ)(1+ϕ)c_e^* = \frac{2+3\phi}{(1+2\phi)(1+\phi)}ce∗​=(1+2ϕ)(1+ϕ)2+3ϕ​. At ce∗c_e^*ce∗​ the slope ϕ(1+(1+ϕ)c)/[(1+ϕ)(2+(1+ϕ)c)]\phi(1+(1+\phi)c)/[(1+\phi)(2+(1+\phi)c)]ϕ(1+(1+ϕ)c)/[(1+ϕ)(2+(1+ϕ)c)] of the best response (2) equals −1-1−1, the linear system wi=w^i(wj)w_i = \hat w_i(w_j)wi​=w^i​(wj​) is singular, and every profile has a continuum of equilibria (for instance w1,2=wˉ±tw_{1,2} = \bar w \pm tw1,2​=wˉ±t when n=0n = 0n=0) with different profits; the proof of Lemma 1 (p. 260) overlooks this. Existence holds for every cec_ece​.

Preamble
import Mathlib
import Definitions.Def_InfoSharing_Shared_IsSignalModel
import Definitions.Def_InfoSharing_Shared_PayoffTable
import Definitions.Def_InfoSharing_Shared_ClosedForms
open MeasureTheory
open InfoSharing.Shared
Formal statement
namespace InfoSharing.Economy

/-- **Lemma 1** (Shang, Ha & Tong 2016, p. 251), production economy (`c = −c_e`) under the
Assumption `c_e < 2/(1+φ)` (p. 251). For every information-status profile `X` the pricing stage
has an equilibrium, and (for `c_e ≠ (2+3φ)/((1+2φ)(1+φ))`, see below) in every equilibrium
manufacturer `i`'s wholesale price is
`w̄ + α_w · Y` and the retail price of product `i` is `p̄ + α_p · Y` (a.s.), with the
coefficients of the lemma (`alphaW`, `alphaP`, which depend on `n` and on `X i`).

**Correction.** Uniqueness is asserted for `c_e ≠ (2+3φ)/((1+2φ)(1+φ))`. At that value the
slope `φ(1+(1+φ)c)/((1+φ)(2+(1+φ)c))` of the best response (2) equals `−1`, the linear system
`w_i = ŵ_i(w_j)` is singular, and every profile has a continuum of equilibria; the paper's
uniqueness claim (proof of Lemma 1, p. 260) fails there. Existence holds for all `c_e`. -/
theorem lemma_1_pricing_equilibrium (φ ce c a b σ β : ℝ) {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (θ Y : Ω → ℝ) (hφ : 0 < φ) (hc : c = -ce) (hce : 0 < ce)
    (hA : ce < 2 / (1 + φ)) (hM : IsSignalModel μ θ Y σ β) (X : Fin 2 → Status) :
    (∃ (ρ : (Fin 2 → ℝ) → ℝ → (Fin 2 → ℝ)) (f : Fin 2 → ℝ → ℝ),
      IsPricingEq μ θ Y a b c φ β X ρ f) ∧
    (ce ≠ (2 + 3 * φ) / ((1 + 2 * φ) * (1 + φ)) → ∀ (ρ : (Fin 2 → ℝ) → ℝ → (Fin 2 → ℝ)) (f : Fin 2 → ℝ → ℝ),
      IsPricingEq μ θ Y a b c φ β X ρ f → ∀ i : Fin 2,
        (∀ᵐ ω ∂μ, f i (Y ω) = wbar a b c φ + alphaW c φ β X i * Y ω) ∧
        (∀ᵐ ω ∂μ, ρ (fun j => f j (Y ω)) (Y ω) i = pbar a b c φ + alphaP c φ β X i * Y ω)) := by sorry

end InfoSharing.Economy
Source
Shang, Ha & Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Sci. 62(1) 2016, p. 251, Lemma 1 (with wˉ\bar wwˉ, pˉ\bar ppˉ​ from the paragraph above it)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me