(19), p. 15 — the manufacturer's unique best response is e* = p(1 − (1 − β)p)/(2(1 − α)k)
ProvedRareDisease.ExogOutcome.best_responsebest-responseoutcome-based-paymentp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1subsidy
Consider Setting (2B) with R&D cost scale and consortium price . For every subsidy policy , the manufacturer's profit has exactly one maximizer over , namely
This is the follower's response in the Stackelberg game; every statement about the government's problem evaluates welfare and spending at this efficacy.
Formalization Note The best-response set is the set of maximizers over , and the theorem says it equals the singleton , i.e. both existence and uniqueness. The hypotheses and are the paper's standing assumptions made explicit: with and the bracket is not positive and no maximizer with exists. The page says "Equation (10)"; the manufacturer's objective is (9).
Preamble
import Mathlib import Definitions.Def_RareDisease_ExogOutcome_Setting
Formal statement
namespace RareDisease.ExogOutcome
/-- (19), p. 15: in Setting (2B) the manufacturer's best response is unique and equals
`e* = p (1 - (1 - β) p) / (2 (1 - α) k)`. -/
theorem best_response (k p α β : ℝ) (hk : 0 < k) (hp0 : 0 < p) (hp1 : p < 1)
(hpol : RareDisease.Endogenous.IsPolicy α β) :
BR k p α β = {p * (1 - (1 - β) * p) / (2 * (1 - α) * k)} := by sorry
end RareDisease.ExogOutcome
Source
Olsder, Martagan, Tang, Improving Access to Rare Disease Treatments: Optimal Subsidies, Pricing, and Payment, SSRN working paper 3481150 (version of 2019-11-13), p. 15, (19)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.