Appendix (4) — the limit of $U(p,x)$ as $p\to1$ is $u(\mu_x)+\tfrac{\sigma_x^2}{2}\lim_{y\to-\infty}u''(y)$

Proved

RobustMeanCov.OnePoint.twoPointValue_tendsto_one

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

limitsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1two-point-distribution

Let $u:\mathbb R\to\mathbb R$ be concave and twice differentiable with convex derivative $u'$ , let $m\in\mathbb R$ and $s>0$ , and let $U(p)$ be the two-point objective (8) with mean $m$ and standard deviation $s$ .

If $u''(y)\to L\in\mathbb R$ as $y\to-\infty$ , then

\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\,L .

If $u''(y)\to-\infty$ as $y\to-\infty$ , then $U(p)\to-\infty$ as $p\to1^-$ .

Since each $U(p)$ is the expected utility of a law in $\mathbb M_{(m,s^2)}$ , this yields the upper bound (4) of the appendix, $U(x)\le u(\mu_x)+\frac{\sigma_x^2}{2}\lim_{y\to-\infty}u''(y)$ , and in the second case shows $U(x)=-\infty$ .

Formalization Note Under these hypotheses $u''$ is nondecreasing and nonpositive, so its limit at $-\infty$ is either finite or $-\infty$ ; the two cases are stated separately with explicit limit hypotheses.

Preamble

import Mathlib
import Definitions.Def_RobustMeanCov_OnePoint_twoPointValue
open Filter Topology

Formal statement

namespace RobustMeanCov.OnePoint

theorem twoPointValue_tendsto_one (u : ℝ → ℝ) (hconc : ConcaveOn ℝ Set.univ u)
    (hu : Differentiable ℝ u) (hu' : Differentiable ℝ (deriv u))
    (hconv : ConvexOn ℝ Set.univ (deriv u)) (m s : ℝ) (hs : 0 < s) :
    (∀ L : ℝ, Tendsto (deriv (deriv u)) atBot (𝓝 L) →
      Tendsto (twoPointValue u m s) (𝓝[<] 1) (𝓝 (u m + s ^ 2 / 2 * L))) ∧
    (Tendsto (deriv (deriv u)) atBot atBot →
      Tendsto (twoPointValue u m s) (𝓝[<] 1) atBot) := by sorry

end RobustMeanCov.OnePoint

Source

Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Oper. Res. 55(1), 2007, p. 110, Appendix, proof of Proposition 7, (4) and the display preceding it

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

This is a theorem. Let $u:\mathbb{R}\to\mathbb{R}$ satisfy four hypotheses:

$u$ is concave on $\mathbb{R}$ ;
$u$ is differentiable everywhere;
its derivative $u'$ is differentiable everywhere, with derivative $u''$ ;
$u'$ is convex on $\mathbb{R}$ .

Let $m$ be any real number and let $s>0$ . Define $V(p) = p\,u\!\left(m+\sqrt{(1-p)/p}\,s\right) + (1-p)\,u\!\left(m-\sqrt{p/(1-p)}\,s\right)$ . The theorem asserts both of the following:

For every real number $L$ : if $u''(y)\to L$ as $y\to-\infty$ , then

\lim_{p\to1^-} V(p) = u(m) + \frac{s^2}{2}\,L .

If $u''(y)\to-\infty$ as $y\to-\infty$ , then $V(p)\to-\infty$ as $p\to1^-$ .

Both parts are conditional. If $u''$ has neither a finite limit nor the limit $-\infty$ as $y\to-\infty$ , the theorem asserts nothing about $V$ . The limits are taken from the left only, over $p<1$ ; the value of $V$ at $p=1$ itself is irrelevant. Nothing is said about $p\to0^+$ or about behaviour as $y\to+\infty$ . The requirement $s>0$ is strict, so $s=0$ and negative $s$ are not covered.

Human review

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

View graph

Appendix (4) — the limit of U(p,x)U(p,x)U(p,x) as p→1p\to1p→1 is u(μx)+σx22lim⁡y→−∞u′′(y)u(\mu_x)+\tfrac{\sigma_x^2}{2}\lim_{y\to-\infty}u''(y)u(μx​)+2σx2​​limy→−∞​u′′(y)

Appendix (4) — the limit of $U(p,x)$ as $p\to1$ is $u(\mu_x)+\tfrac{\sigma_x^2}{2}\lim_{y\to-\infty}u''(y)$