Jensen's Inequality

Statement

Let $\varphi : \mathbb{R} \to \mathbb{R}$ be a convex function and $X$ an integrable real-valued random variable. Then:

Equivalently, in finite-weight form: if $w_1, \ldots, w_n \geq 0$ with $\sum w_i = 1$ and $x_1, \ldots, x_n \in \mathbb{R}$, then:

Visualization

Take $\varphi(x) = x^2$ (convex) and a fair die: $X \in \{1,2,3,4,5,6\}$, each with weight $1/6$.

Mean first, then square:

Square first, then average:

$x$	$x^2$	weight $w$	$w \cdot x^2$
1	1	1/6	1/6
2	4	1/6	4/6
3	9	1/6	9/6
4	16	1/6	16/6
5	25	1/6	25/6
6	36	1/6	36/6

Jensen: $12.25 \leq 15.17$. The gap $E[X^2] - (E[X])^2 = \text{Var}(X)$ is exactly the variance.

Proof Sketch

1. Tangent line at the mean. Because $\varphi$ is convex, there exists a supporting hyperplane (tangent) at $\mu = E[X]$: a constant $c$ such that $\varphi(t) \geq \varphi(\mu) + c(t - \mu)$ for all $t$.
2. Substitute $t = X$. Pointwise: $\varphi(X) \geq \varphi(\mu) + c(X - \mu)$.
3. Take expectations. $E[\varphi(X)] \geq \varphi(\mu) + c \cdot (E[X] - \mu) = \varphi(\mu)$.

The discrete version follows the same idea with weighted sums replacing integrals.

Connections

Jensen's inequality extends Cauchy–Schwarz InequalityCauchy–Schwarz Inequality$$|\langle u, v \rangle| \leq \|u\| \, \|v\|$$The inner product of two vectors is bounded by the product of their normsRead more → to general convex functions: Cauchy–Schwarz is Jensen applied to $\varphi(t) = t^2$ with a specific pairing. It also underpins the AM–GM InequalityAM–GM Inequality$$\frac{a_1+\cdots+a_n}{n} \geq \sqrt[n]{a_1 \cdots a_n}$$The arithmetic mean is always at least as large as the geometric meanRead more →: apply Jensen to $\varphi = -\log$ (convex) with uniform weights to obtain $\log(\bar x) \geq \overline{\log x}$, i.e., AM $\geq$ GM.

Lean4 Proof

The discrete finite-weight form lives in Mathlib.Analysis.Convex.Jensen as ConvexOn.map_sum_le.

ConvexOn.map_sum_le is proved in Mathlib by induction on the finite set, applying the two-point convexity condition at each step.

import Mathlib.Analysis.Convex.Jensen

namespace MoonMath

open Finset

/-- **Jensen's inequality** (finite discrete form).
    For a convex function `φ` on a convex set `s`, non-negative weights summing to 1,
    and points in `s`, `φ(Σ w_i x_i) ≤ Σ w_i φ(x_i)`. -/
theorem jensen_discrete {ι : Type*} (t : Finset ι)
    {φ : ℝ → ℝ} {s : Set ℝ} (hφ : ConvexOn ℝ s φ)
    {w : ι → ℝ} {x : ι → ℝ}
    (hw : ∀ i ∈ t, 0 ≤ w i) (hw1 : ∑ i ∈ t, w i = 1)
    (hx : ∀ i ∈ t, x i ∈ s) :
    φ (∑ i ∈ t, w i • x i) ≤ ∑ i ∈ t, w i • φ (x i) :=
  hφ.map_sum_le hw hw1 hx

end MoonMath