Lemma C.1, p. 47 — if L-funds are raised, then R̄*_PE,L = 1 + r(λ, δ_L)

Proved

PELiquidity.Primary.lemma_C_1

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

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

Fix the model parameters and a capital share $\mu_H\in(0,1)$ of $H$ -LPs. In every private equity market equilibrium without a secondary market in which $L$ -funds are raised, $\alpha^*_L>0$ , the return to $L$ -LPs equals their break-even return:

\bar R^*_{PE,L}=1+r(\lambda,\delta_L).

$L$ -LPs therefore earn no rent whenever they are in the market; any return premium in equilibrium accrues to $H$ -LPs.

Preamble

import Mathlib
import Definitions.Def_PELiquidity_Primary_Setting
import Definitions.Def_PELiquidity_Primary_Market

Formal statement

namespace PELiquidity.Primary

/-- Lemma C.1: in an equilibrium without a secondary market, if L-funds are raised
(`α*_L > 0`) then L-LPs earn exactly their break-even return `1 + r(λ, δ_L)`. -/
theorem lemma_C_1 (P : Params) (muH : ℝ) (hmu0 : 0 < muH) (hmu1 : muH < 1) (E : Allocation)
    (hE : IsEquilibrium P muH E) (hαL : 0 < E.αL) :
    E.RL = grossReturn P.lam P.δL := by sorry

end PELiquidity.Primary

Source

Maurin, Robinson & Strömberg, A Theory of Liquidity in Private Equity, working paper (draft of December 2020), p. 47, Appendix C.3, Lemma C.1

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