Lemma 1 — the unique pricing equilibrium is linear in the demand signal (production economy)
ProvedInfoSharing.Economy.lemma_1_pricing_equilibriumLet and , put , and let be reals. Let satisfy the signal model with variance and weight . For every status profile the pricing game of §4.1 has an equilibrium, and, provided (see the note), in every equilibrium , for each manufacturer , almost surely
where , , and , are the coefficients of Lemma 1 selected by and, when , by :
- , , ;
- , , .
An informed manufacturer's wholesale price responds to the signal, positively when and negatively when ; an uninformed one's does not. All ex ante profits of §4.2 follow from this equilibrium.
Formalization Note The production economy model takes with (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 (the paper's cap at is assumed never to bind, footnote 11, p. 251). Correction of the paper. Uniqueness is asserted only for . At the slope of the best response (2) equals , the linear system is singular, and every profile has a continuum of equilibria (for instance when ) with different profits; the proof of Lemma 1 (p. 260) overlooks this. Existence holds for every .
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
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.