Proof of Lemma 3, p. 28 — every response coefficient satisfies C^{X_jX_i}_j < 1

Proved

CompetingChains.Cournot.lemma_3_coeff_lt_one

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

cournot-competitioninformation-sharingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain

Let $k>1/3$ , $0\le\gamma_C<1$ , $t>0$ and $\sigma^2>0$ , and let $C^{X_iX_j}$ be the Cournot response coefficients of Lemma 2(a). Then for all arrangements $X_i,X_j\in\{S,N\}$ ,

C^{X_iX_j}<1 .

In the paper this gives the sign of the wholesale price and cost-reduction coefficients (Lemma 3(a)); in this mission it guarantees $1-\gamma_C C_j>0$ , which the comparisons of profits use.

Preamble

import Mathlib
import Definitions.Def_CompetingChains_Cournot_Setting

Formal statement

namespace CompetingChains.Cournot

theorem lemma_3_coeff_lt_one (k γ t σsq : ℝ) (hk : 1 / 3 < k) (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
    (ht : 0 < t) (hσ : 0 < σsq) :
    ∀ Xi Xj : Arrangement, C k γ t σsq Xi Xj < 1 := by sorry

end CompetingChains.Cournot

Source

Ha, Tian & Tong, Information Sharing in Competing Supply Chains with Production Cost Reduction (MSOM 2017, pre-published version), p. 28, proof of Lemma 3, first sentence

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph