Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

(B.4), p. 42 — the mean-variance objective qq_N − (γ/2)q²q_D is maximized exactly at q = q_N/(γq_D)

Proved
InfoRegimes.MarketEq.mean_variance_demand

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

asset-pricingmean-varianceoptimal-demandp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let γ>0\gamma > 0γ>0 be a risk aversion parameter, qD>0q_D > 0qD​>0 the expected conditional variance of the net profit per share, and qN∈Rq_N \in \mathbb RqN​∈R its conditional expectation. The mean-variance objective

q↦q qN−γ2q2qDq \mapsto q\,q_N - \frac{\gamma}{2}q^2 q_Dq↦qqN​−2γ​q2qD​

attains its maximum over q∈Rq \in \mathbb Rq∈R at qqq if and only if

q=1γ qNqD.q = \frac{1}{\gamma}\,\frac{q_N}{q_D}.q=γ1​qD​qN​​.

This is the first-order condition (B.4) of the investor problem (B.1): the optimal demand of each investor type is its expected net profit divided by γ\gammaγ times its expected conditional variance. It identifies the maximizers required by market clearing in the model with the demand formulas (B.6).

Preamble
import Mathlib
Formal statement
namespace InfoRegimes.MarketEq

theorem mean_variance_demand (γ qD qN q : ℝ) (hγ : 0 < γ) (hqD : 0 < qD) :
    IsMaxOn (fun x : ℝ => x * qN - γ / 2 * x ^ 2 * qD) Set.univ q ↔ q = qN / (γ * qD) := by sorry

end InfoRegimes.MarketEq
Source
Glasserman, Mamaysky & Shen, Dynamic Information Regimes in Financial Markets, SSRN 3324789 (version of October 17, 2023), p. 42, eq. (B.4)
Human review
  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 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