Equation (3), p. 10 — supplier profit at the quantity equilibrium

Proved

CrossLicensing.ExPost.equation_3

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

cournotcross-licensingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1supplier-profit

Fix $0\le\beta\le1$ , $0\le T_1\le T_2$ , and $r\ge0$ , and let $(q_1,q_2)$ be any Nash equilibrium of the quantity game (1). With $r_1=1+T_1(2-\beta)-T_2(1-2\beta)$ and $r_2=1+\beta T_1+T_2$ , the supplier's profit is

r(q_1+q_2)=\pi_s^{\mathrm{cl}}(r)=\begin{cases} \dfrac{(2-2r+(T_1+T_2)(1+\beta))r}{3},&r\le r_1,\\ \dfrac{(1-r+\beta T_1+T_2)r}{2},&r_1<r\le r_2,\\ 0,&r>r_2. \end{cases}

This connects the supplier's actual revenue at a strategic outcome to the paper's piecewise expression. At $\beta=0$ it gives equation (4), the no-licensing profit. Formalization Note The result applies to every Nash equilibrium; equilibrium existence is supplied by equation (2).

Preamble

import Mathlib
import Definitions.Def_CrossLicensing_ExPost_Model

Formal statement

namespace CrossLicensing.ExPost

/-- Equation (3), the supplier's profit at any quantity-game equilibrium. -/
theorem equation_3 (β T₁ T₂ r : ℝ) (h : Standing β T₁ T₂ r) (q : ℝ × ℝ)
    (hq : IsQuantityNE β T₁ T₂ r q) :
    supplierProfit r q = supplierProfitFormula β T₁ T₂ r := by sorry

end CrossLicensing.ExPost

Source

Wang, Huang, Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN 3053682 (version of 2023-04-27), p. 10, equation (3), with equation (4) at beta = 0

Human review

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

View graph