Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

(19), p. 15 — the manufacturer's unique best response is e* = p(1 − (1 − β)p)/(2(1 − α)k)

Proved
RareDisease.ExogOutcome.best_response

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

best-responseoutcome-based-paymentp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1subsidy

Consider Setting (2B) with R&D cost scale k>0k>0k>0 and consortium price p∈(0,1)p\in(0,1)p∈(0,1). For every subsidy policy (α,β)∈[0,1)2(\alpha,\beta)\in[0,1)^2(α,β)∈[0,1)2, the manufacturer's profit e p [1−(1−β)p]−(1−α)ke2e\,p\,[1-(1-\beta)p]-(1-\alpha)ke^2ep[1−(1−β)p]−(1−α)ke2 has exactly one maximizer over e>0e>0e>0, namely

e∗=p (1−(1−β)p)2(1−α)k.e^* = \frac{p\,(1-(1-\beta)p)}{2(1-\alpha)k}.e∗=2(1−α)kp(1−(1−β)p)​.

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 e>0e>0e>0, and the theorem says it equals the singleton {e∗}\{e^*\}{e∗}, i.e. both existence and uniqueness. The hypotheses k>0k>0k>0 and 0<p<10<p<10<p<1 are the paper's standing assumptions made explicit: with p≥1p\ge1p≥1 and β=0\beta=0β=0 the bracket 1−(1−β)p1-(1-\beta)p1−(1−β)p is not positive and no maximizer with e>0e>0e>0 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
  • 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

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