Sec. 4.2.2, p. 24 — π_s(w(φ), φ) = (1 − c)²/(4(1 + φ(1 − 2τ²)))

Proved

RevShareCoord.Effort.Linear.supplier_profit_closed_form

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

contractsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-sharingsupply-chain

In the linear example, let $0 \le \tau < 1$ , $0 < c < 1$ and $0 < \phi \le 1$ . At the wholesale price $w(\phi) = \phi\big((1-\tau^2)\phi + c(1-\phi\tau^2)\big)/\big(1 + \phi(1-2\tau^2)\big)$ , with the retailer ordering $q(w(\phi), \phi)$ and exerting effort $e = \phi\tau q$ , the supplier's profit simplifies to

\pi_s(w(\phi), \phi) = \frac{(1 - c)^2}{4\big(1 + \phi(1 - 2\tau^2)\big)} .

This closed form is what the comparison of revenue-sharing and wholesale-price contracts rests on.

Preamble

import Mathlib
import Definitions.Def_RevShareCoord_Effort_Linear

Formal statement

namespace RevShareCoord.Effort.Linear

/-- Sec. 4.2.2, p. 24: at the wholesale price `w(φ)` the supplier's profit simplifies to
`π_s(w(φ), φ) = (1 − c)²/(4(1 + φ(1 − 2τ²)))`. -/
theorem supplier_profit_closed_form (τ c φ : ℝ) (hτ0 : 0 ≤ τ) (hτ1 : τ < 1)
    (hc0 : 0 < c) (hc1 : c < 1) (hφ0 : 0 < φ) (hφ1 : φ ≤ 1) :
    supplierProfitAt τ c φ (wholesalePrice τ c φ) =
      (1 - c) ^ 2 / (4 * (1 + φ * (1 - 2 * τ ^ 2))) := by sorry

end RevShareCoord.Effort.Linear

Source

Cachon, Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper (June 2000), p. 24 (PDF p. 25), Section 4.2.2, 'The supplier profit function simplifies to π_s(w(φ), φ) = (1 − c)²/(4(1 + φ(1 − 2τ²)))'

Human review

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

View graph