Appendix (5) — the quadratic $\tfrac12u''(-\infty)(y-\mu_x)^2+u'(\mu_x)(y-\mu_x)+u(\mu_x)$ supports $u$

Proved

RobustMeanCov.OnePoint.quadratic_five_supports

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

limitsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1supporting-quadratic

Let $u:\mathbb R\to\mathbb R$ be concave and twice differentiable with convex derivative $u'$ , and suppose $u''(y)\to L\in\mathbb R$ as $y\to-\infty$ . Fix $m\in\mathbb R$ and let $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ for $y\neq m$ . Then

the quadratic (5)

q(y)=\tfrac12 L\,(y-m)^2+u'(m)(y-m)+u(m)

supports $u$ : $q(y)\le u(y)$ for every $y\in\mathbb R$ ; 2. $\inf_{y\neq m}d(y)=\tfrac12 L$ , i.e. $\tfrac12L$ is the greatest lower bound of $\{d(y):y\ne m\}$ ; 3. $d(y)\to\tfrac12L$ as $y\to-\infty$ .

For every law of mean $m$ and variance $s^2$ one has $E[q(r)]=u(m)+\frac{s^2}{2}L$ , so with Proposition 3 this gives the lower bound matching (4) in the proof of Proposition 7(a).

Formalization Note $L$ is the paper's $u''(-\infty)$ , taken as an explicit finite limit hypothesis.

Preamble

import Mathlib
open Filter Topology

Formal statement

namespace RobustMeanCov.OnePoint

theorem quadratic_five_supports (u : ℝ → ℝ) (hconc : ConcaveOn ℝ Set.univ u)
    (hu : Differentiable ℝ u) (hu' : Differentiable ℝ (deriv u))
    (hconv : ConvexOn ℝ Set.univ (deriv u)) (L : ℝ)
    (hL : Tendsto (deriv (deriv u)) atBot (𝓝 L)) (m : ℝ) :
    (∀ y : ℝ, 1 / 2 * L * (y - m) ^ 2 + deriv u m * (y - m) + u m ≤ u y) ∧
    IsGLB ((fun y : ℝ => (u y - u m) / (y - m) ^ 2 - deriv u m / (y - m)) '' {y | y ≠ m})
      (1 / 2 * L) ∧
    Tendsto (fun y : ℝ => (u y - u m) / (y - m) ^ 2 - deriv u m / (y - m)) atBot
      (𝓝 (1 / 2 * L)) := 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, (5) and the paragraph following 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;
$u'$ is differentiable everywhere, with derivative $u''$ ;
$u'$ is convex on $\mathbb{R}$ .

Let $L$ be a real number with $u''(y)\to L$ as $y\to-\infty$ , and let $m$ be any real number. Define, for $y \ne m$ ,

g(y) = \frac{u(y)-u(m)}{(y-m)^2} - \frac{u'(m)}{y-m}.

The theorem asserts all three of the following:

For every real $y$ ,

\tfrac12 L\,(y-m)^2 + u'(m)\,(y-m) + u(m) \;\le\; u(y).

$\tfrac12 L$ is the greatest lower bound of the set $\{\,g(y) : y\in\mathbb{R},\ y\neq m\,\}$ . That is, $\tfrac12 L \le g(y)$ for every $y\ne m$ , and every lower bound of this set is $\le \tfrac12 L$ .
$g(y)\to\tfrac12 L$ as $y\to-\infty$ .

Degenerate cases:

Infimum, not minimum. Item 2 asserts an infimum. It does not say that $\tfrac12 L$ is attained.
The point $y=m$ is excluded from the set in item 2. Under the division-by-zero convention, $g(m)$ would be $0$ .
The quadratic in item 1 equals $u(m)$ at $y=m$ .
Missing limit. If $u''$ has no finite limit at $-\infty$ , the theorem does not apply.
No behaviour as $y\to+\infty$ is asserted.

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 (5) — the quadratic 12u′′(−∞)(y−μx)2+u′(μx)(y−μx)+u(μx)\tfrac12u''(-\infty)(y-\mu_x)^2+u'(\mu_x)(y-\mu_x)+u(\mu_x)21​u′′(−∞)(y−μx​)2+u′(μx​)(y−μx​)+u(μx​) supports uuu

Appendix (5) — the quadratic $\tfrac12u''(-\infty)(y-\mu_x)^2+u'(\mu_x)(y-\mu_x)+u(\mu_x)$ supports $u$