Proposition 5: an inverse S-shaped derivative with finite limits gives two-point support

Proved

RobustMeanCov.TwoPoint.two_point_support_of_inverse_S_shaped_deriv

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

distributionally-robustp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1real-analysistwo-point-support

Let $u:\mathbb R\to\mathbb R$ be differentiable, and suppose its derivative $u'$ is inverse S-shaped — decreasing, concave on $(-\infty,x_0)$ and convex on $(x_0,\infty)$ for some $x_0$ — with finite limits

\lim_{y\to-\infty}u'(y)\in\mathbb R,\qquad \lim_{y\to+\infty}u'(y)\in\mathbb R .

Then $u$ satisfies the two-point support property: for every $\mu\in\mathbb R$ and $\sigma>0$ there are $a<b$ and a quadratic $q\le u$ with $q(a)=u(a)$ , $q(b)=u(b)$ , and a law with mean $\mu$ , variance $\sigma^2$ and support $\{a,b\}$ .

Consequently, for such $u$ , the worst-case expected utility over all laws with mean $\mu$ and variance $\sigma^2$ reduces to a one-dimensional minimization over two-point laws (Proposition 4 of the paper). Examples include the log-logistic function $u(x)=C+\log\frac{1}{1+e^{-ax}}$ and the catenary $u(x)=C-b\cosh(ax)$ plus a concave quadratic.

Formalization Note "Decreasing" is strict (StrictAnti after unfolding IsInverseSShaped), the paper's reading of "increasing" in Definition 2. No continuity of $u'$ is assumed beyond what the hypotheses imply.

Preamble

import Mathlib
import Definitions.Def_RobustMeanCov_TwoPoint_SShaped
import Definitions.Def_RobustMeanCov_TwoPoint_TwoPointSupport
open Filter Topology

Formal statement

namespace RobustMeanCov.TwoPoint

/-- Proposition 5 (Popescu 2007, p. 102): if `u` is differentiable and `u'` is inverse S-shaped
with finite limits at `±∞`, then `u` satisfies the two-point support property. -/
theorem two_point_support_of_inverse_S_shaped_deriv (u : ℝ → ℝ) (hu : Differentiable ℝ u)
    (hinv : IsInverseSShaped (deriv u))
    (hbot : ∃ l : ℝ, Tendsto (deriv u) atBot (𝓝 l))
    (htop : ∃ l : ℝ, Tendsto (deriv u) atTop (𝓝 l)) :
    TwoPointSupport u := by sorry

end RobustMeanCov.TwoPoint

Source

Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Oper. Res. 55(1), 2007, p. 102, Proposition 5; proof in the Appendix, p. 110

Read-back

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

Let $u:\mathbb{R}\to\mathbb{R}$ be any real function. The statement makes three assumptions about $u$ :

(H1) Differentiability. $u$ is differentiable at every point of $\mathbb{R}$ . Write $u'$ for its derivative. Under (H1), $u'(x)$ is the true derivative at every $x$ , so the default value $0$ that Lean assigns at points of non-differentiability never occurs.
(H2) Inverse S-shape. The derivative $u'$ satisfies the predicate IsInverseSShaped. This predicate is defined in the imported bundle file Def_RobustMeanCov_TwoPoint_SShaped. Its definition is not part of the code given to this read-back, so its content cannot be expanded here. The theorem asserts exactly what that definition says, whatever it is. It carries no meaning beyond its name, and a reader must check the definition itself.
(H3) Finite limits at both ends. There exist real numbers $\ell_-$ and $\ell_+$ with

\lim_{x\to-\infty}u'(x)=\ell_-\qquad\text{and}\qquad\lim_{x\to+\infty}u'(x)=\ell_+ .

Both limits are finite real numbers, not $\pm\infty$ . The statement does not require $\ell_-$ and $\ell_+$ to be equal or different, and it does not fix their signs.

Conclusion. Under (H1)–(H3), $u$ satisfies the predicate TwoPointSupport. That predicate is defined in the imported file Def_RobustMeanCov_TwoPoint_TwoPointSupport. Its definition is also not included in the code given here, so the conclusion is exactly " $u$ has the property named TwoPointSupport", whatever that definition asserts. In particular, this read-back cannot say what optimization problem, which distributions, or which moment constraints the property involves.

What the statement does not assume. It does not require that:

$u'$ is continuous;
$u$ is monotone, concave or convex;
$u$ is bounded;
$u$ has any integrability property.

Any such condition applies only if it is built into one of the two named predicates.

Degenerate cases. The only variable is the function $u$ on $\mathbb{R}$ , so there are no empty or one-element types, no counts or horizons that could be zero, and no division or subtraction in $\mathbb{N}$ in the statement itself. Because of (H1), the derivative never takes Lean's default value. The limits in (H3) are finite by construction, so no infinite or undefined limit arises.

Whether the statement could hold vacuously depends entirely on IsInverseSShaped, which cannot be seen here. If no derivative of an everywhere-differentiable function with finite limits at $\pm\infty$ can satisfy that predicate, the hypotheses can never be met and the theorem says nothing. One example: a predicate that demands behaviour a bounded-at-the-ends derivative cannot have.

At the other extreme, if the predicate is satisfied by constant functions, then $u(x)=ax+b$ with $u'\equiv a$ satisfies (H1) and (H3) with $\ell_-=\ell_+=a$ . The theorem would then claim that every affine $u$ has TwoPointSupport.

Both points must be settled by reading the two definition files.

Human review

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

View graph