Appendix B, proof of Proposition 2, p. 52 — the incentive constraint (6) holds exactly when e = πx

Proved

LeveragedPayouts.Unregulated.ic_effort

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

moral-hazardoptimizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\pi>0$ and let $x,e$ be real numbers. The effort $e$ maximizes the shareholder's net utility $y\mapsto xy-y^2/(2\pi)$ if and only if

e=\pi x.

This is the first step of the proof of Proposition 2: it turns the incentive constraint (6)/(32) into an explicit formula, so that the firm's program reduces to a choice of the retained stake $x$ and of investment.

Preamble

import Mathlib
import Definitions.Def_LeveragedPayouts_Unregulated_Firm

Formal statement

namespace LeveragedPayouts.Unregulated
theorem ic_effort (π : ℝ) (hπ : 0 < π) (x e : ℝ) : IsIC π x e ↔ e = π * x := by sorry
end LeveragedPayouts.Unregulated

Source

Acharya & Plantin, Monetary Easing, Leveraged Payouts, and Lack of Investment, SSRN 3484935 (version of May 23, 2023), p. 52, Appendix B, proof of Proposition 2

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph