Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition IA.1, p. IA2 — mean-optimal intensity tends to one

Proved
RiskEU.RobustShrink.proposition_IA_1_limit

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

asymptoticsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1portfolio-choice

Fix the number of stocks NNN, risk aversion γ\gammaγ, population variances σg2\sigma_g^2σg2​ and ψ2\psi^2ψ2, GMV mean μg\mu_gμg​, and robustness weight λ\lambdaλ. If N≥2N\geq2N≥2, γ>0\gamma>0γ>0, σg2>0\sigma_g^2>0σg2​>0, and ψ2>0\psi^2>0ψ2>0, then the mean-maximizing intensity in (IA3) obeys

lim⁡T→∞κE(T)=1.\lim_{T\to\infty}\kappa_E(T)=1.T→∞lim​κE​(T)=1.

This gives the asymptotic mean benchmark for the robust shrinkage intensity.

Formalization Note The paper omits the necessary condition ψ2>0\psi^2>0ψ2>0: at ψ2=0\psi^2=0ψ2=0, formula (IA3) gives κE(T)=0\kappa_E(T)=0κE​(T)=0. The estimator-consistency sentence requires a sample-portfolio model and is outside this closed-form result. The OOSU moments are the closed forms from Proposition IA.1 and Proposition 1; their probabilistic identification is outside this mission.

Preamble
import Mathlib
import Definitions.Def_RiskEU_RobustShrink_Setting
Formal statement
namespace RiskEU.RobustShrink

/-- Proposition IA.1, final sentence, p. IA2: the mean-optimal intensity tends to one. -/
theorem proposition_IA_1_limit (p : Params) (hp : p.Standing)
    (hpsi : 0 < p.psi2) :
    Filter.Tendsto (fun T : ℕ => p.kappaE T) Filter.atTop (nhds 1) := by sorry

end RiskEU.RobustShrink
Source
Lassance, Martín-Utrera, Simaan, The Risk of Expected Utility under Parameter Uncertainty, SSRN 3855546 (version dated August 18, 2023), Proposition IA.1, final sentence, p. IA2
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