Proof of Lemma 2(a), p. 28 — the linear strategies with coefficients C^{X_iX_j} solve the best responses (7) and (9)
ProvedCompetingChains.Cournot.lemma_2a_fixed_pointLet , , , , and let be the signal weight, so that . Let and let be the response coefficients of Lemma 2(a). If chain plays , then and . The claim is that chain 's linear strategy is a best response: for all arrangements and every signal value ,
where is the best response (7) and the best response (9).
This is the existence half of Lemma 2(a) for the quantities: the pair of linear strategies is a Bayesian equilibrium of the quantity stage. The coefficients are the inputs of every profit formula of the mission.
Formalization Note The conditional expectations are substituted by their values under the linear information structure (p. 8), so the statement is an identity between closed forms. The page cites only (7); for the relevant best response is (9), which is what is stated. Uniqueness, delegated by the paper to Ha et al. (2011), is not stated; the wholesale price and cost reduction lines of Lemma 2(a) are not stated.
import Mathlib import Definitions.Def_CompetingChains_Cournot_Setting
namespace CompetingChains.Cournot
theorem lemma_2a_fixed_point (a c k γ t σsq : ℝ) (hk : 1 / 3 < k) (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
(ht : 0 < t) (hσ : 0 < σsq) :
∀ (Xi Xj : Arrangement) (y : ℝ),
qbar a c k γ + C k γ t σsq Xi Xj * y =
br a c k γ Xi (sig t σsq * y)
(qbar a c k γ + C k γ t σsq Xj Xi * (sig t σsq * y)) (qbar a c k γ) := by sorry
end CompetingChains.Cournot
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.