(C.4), p. 48 — H-market clearing gives μ_H K = I_H − A = (pR − f̄_H)A/(R̄_H − (pR − f̄_H))

Proved

PELiquidity.Primary.fund_size

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

equilibriump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1private-equity

In an equilibrium with $\mu_H\in(0,1)$ , suppose only H-funds are raised and their return $\bar R_H$ exceeds the H-LPs' break-even rate. Write $\bar f_H$ for the expected fee of the optimal H-fund contract and $g=pR-\bar f_H$ for its pledgeable income. Then $0<g<\bar R_H$ , and H-LPs supply all their capital. Market clearing and (3) give the full equation (C.4):

\mu_H K=I_H-A=\frac{gA}{\bar R_H-g}.\qquad\text{(C.4)}

For a fixed fee, the right-hand side is strictly decreasing as the promised return rises above $g$ .

Formalization Note The equilibrium predicate supplies the capital-market and optimal-contract conditions; the theorem makes the market-clearing equality explicit.

Preamble

import Mathlib
import Definitions.Def_PELiquidity_Primary_Setting
import Definitions.Def_PELiquidity_Primary_Market

Formal statement

namespace PELiquidity.Primary

/-- (C.4), Case 2 of Proposition 2: when only H-funds are raised and their
return exceeds H-LPs' break-even return, the H capital supply is `μ_H K`.
Market clearing and (3) give `μ_H K = I_H - A = (pR - f̄_H) A /
(R̄_H - (pR - f̄_H))`. For a fixed fee the contribution falls strictly as
the promised return rises. -/
theorem fund_size (P : Params) (muH : ℝ) (E : Allocation)
    (hmu0 : 0 < muH) (hmu1 : muH < 1) (hE : IsEquilibrium P muH E)
    (hαL : E.αL = 0) (hRH : grossReturn P.lam P.δH < E.RH) :
    let pledge := P.p * P.R - expectedFee P.p P.p E.fH
    0 < pledge ∧ pledge < E.RH ∧
    muH * P.K = E.IH - P.A ∧
    E.IH - P.A = pledge * P.A / (E.RH - pledge) ∧
    StrictAntiOn (fun Rb : ℝ => pledge * P.A / (Rb - pledge))
      (Set.Ioi pledge) := by sorry

end PELiquidity.Primary

Source

Maurin, Robinson & Strömberg, A Theory of Liquidity in Private Equity, working paper (draft of December 2020), p. 48, Appendix C.3, proof of Proposition 2, Case 2, (C.4)

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