Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 14.2: under the wholesale price contract with w>csw > c_sw>cs​ the retailer under-orders, Qr∗<Q0Q^*_r < Q_0Qr∗​<Q0​

Proved
SupplyChainTheory.wholesale_underorder

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

contractsoperations-researchsupply-chainwholesale-price

Theorem 14.2. Under the wholesale price contract, if w>csw > c_sw>cs​ then Qr∗<Q0Q^*_r < Q_0Qr∗​<Q0​: any maximizer of the retailer's profit is strictly smaller than any maximizer of the chain profit.

The retailer absorbs all of the overage risk but only part of the underage risk, since the supplier also pays a stockout penalty, so he orders less than the chain wants. The book omits the proof (Problem 14.6): the retailer's fractile (w+cr−v)/(r−v+pr)(w + c_r - v)/(r - v + p_r)(w+cr​−v)/(r−v+pr​) exceeds the chain's (c−v)/(r−v+p)(c - v)/(r - v + p)(c−v)/(r−v+p) when w>csw > c_sw>cs​, and Fˉ\bar FFˉ is nonincreasing. Only a continuous distribution function and a finite mean are needed.

Preamble
import Definitions.Def_SupplyChainTheory_contracts
Formal statement
namespace SupplyChainTheory

theorem wholesale_underorder (P : ContractData) (D : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure D]
    [MeasureTheory.NullSingletonClass D] (hD : MeasureTheory.Integrable (fun x => x) D) (w : ℝ) (hw : P.cs < w)
    (Qr Q0 : ℝ) (hr : IsMaxOn (retailerProfit P D (wholesaleTransfer w)) Set.univ Qr)
    (h0 : IsMaxOn (chainProfit P D) Set.univ Q0) : Qr < Q0 := by sorry

end SupplyChainTheory
Source
Lawrence V. Snyder and Zuo-Jun Max Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley 2019, DOI 10.1002/9781119584445, p. 570, Sect. 14.5, Theorem 14.2: 'Proof. Omitted; see Problem 14.6'
Human review
  • Endorsed by Shuze Chen · Sep 25, 2026

    Confirmed by the moderator at approval.

  • Endorsed by naimengye · Sep 25, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me