§3.1, Eq. (9): first-order condition for the retailer's optimal effort under a target rebate
ProvedFalseFailureReturns.TargetRebate.rebate_first_order_conditioncontractsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain
Let , , , be as in the model, and let be a target rebate contract with and , with . Suppose an effort maximizes the retailer's expected profit over , and . Then
Equation (9) links , and the induced effort; substituting gives the coordinating contracts (10) and all the profit identities of the appendix.
Formalization Note The paper's "the value that maximizes (8)" is formalized as a maximizer of the true profit (6) over ; the hypotheses (an interior maximizer) and (so that (8) is the profit near ) are the conditions under which the paper's first-order condition applies.
Preamble
import Mathlib import Definitions.Def_FalseFailureReturns_TargetRebate_Model import Definitions.Def_FalseFailureReturns_TargetRebate_UniformRebate
Formal statement
namespace FalseFailureReturns.TargetRebate
theorem rebate_first_order_condition (P : Params) (T u ρs : ℝ)
(ha : 0 < P.a) (hβ : 0 < P.β) (hM : 0 < P.Mm) (hR : 0 < P.Rr)
(hu : 0 < u) (hT : 0 < T) (hρs : 1 < ρs)
(hmax : IsMaxOn (rebateRetailerProfit P T u) (Set.Ici 1) ρs)
(hTlt : T < 2 * P.β / ρs) :
T ^ 2 * u * ρs ^ 2 - 4 * P.a * P.β * ρs ^ 3 + 4 * P.Rr * P.β ^ 2 = 0 := by sorry
end FalseFailureReturns.TargetRebate
Source
Ferguson, Guide & Souza, Supply Chain Coordination for False Failure Returns, MSOM 8(4) 2006, p. 383, §3.1, Eq. (9)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.