[proofplan] The inequality $f^{**} \leq f$ follows directly from the definition of the conjugate: every affine function $x \mapsto x \cdot y - f^*(y)$ lies below $f$. The biconjugate is therefore the supremum of affine lower bounds, hence is convex and lower semicontinuous, with the empty-family convention giving the possible value $-\infty$. For the converse direction, when $f$ is lower semicontinuous and convex, we separate points below the epigraph of $f$ from the closed convex epigraph. Nonvertical separations give affine minorants directly, while horizontal separations are tilted using one fixed affine minorant to produce finite conjugate slopes with arbitrarily large value at the separated point. [/proofplan]

[step:Show that every conjugate affine function lies below $f$] Fix $y \in \mathbb{R}^n$. By definition of $f^*(y)$, for every $x \in \mathbb{R}^n$ we have \begin{align*} x \cdot y - f(x) \leq f^*(y). \end{align*} Equivalently, \begin{align*} x \cdot y - f^*(y) \leq f(x). \end{align*} Taking the supremum over $y \in \mathbb{R}^n$ gives \begin{align*} f^{**}(x) \leq f(x) \end{align*} for every $x \in \mathbb{R}^n$. [/step]

[step:Represent $f^{**}$ as a supremum of continuous affine minorants] Let \begin{align*} Y := \{y \in \mathbb{R}^n : f^*(y) < +\infty\}. \end{align*} For each $y \in Y$, define the affine map \begin{align*} A_y: \mathbb{R}^n \to \mathbb{R}, \qquad A_y(x) := x \cdot y - f^*(y). \end{align*} If $y \notin Y$, then $f^*(y)=+\infty$ and the expression $x \cdot y - f^*(y)$ contributes the constant value $-\infty$ to the supremum. Hence \begin{align*} f^{**}(x) = \sup_{y \in Y} A_y(x) \end{align*} for every $x \in \mathbb{R}^n$, with the convention that the supremum over the empty set is $-\infty$. Each $A_y$ is continuous and affine. A pointwise supremum of affine functions is convex, because for $x_1,x_2 \in \mathbb{R}^n$ and $t \in [0,1]$, \begin{align*} A_y(tx_1+(1-t)x_2) = tA_y(x_1)+(1-t)A_y(x_2) \leq t f^{**}(x_1)+(1-t)f^{**}(x_2) \end{align*} for every $y \in Y$, and taking the supremum over $y \in Y$ gives the convexity inequality. A pointwise supremum of continuous functions is lower semicontinuous, because for each $a \in \mathbb{R}$, \begin{align*} \{x \in \mathbb{R}^n : f^{**}(x) > a\} = \bigcup_{y \in Y} \{x \in \mathbb{R}^n : A_y(x) > a\}, \end{align*} and the right-hand side is open. Thus $f^{**}$ is convex and lower semicontinuous, including the degenerate case $Y=\varnothing$, where $f^{**}\equiv-\infty$. [/step]

[step:Construct one finite affine minorant when $f$ is closed and convex]Assume now that $f$ is convex and lower semicontinuous. Define the epigraph \begin{align*} E := \operatorname{epi} f = \{(z,s) \in \mathbb{R}^n \times \mathbb{R} : f(z) \leq s\}. \end{align*} Since $f$ is proper, choose $x_0 \in \operatorname{dom} f$. Choose $r_0 \in \mathbb{R}$ such that $r_0 < f(x_0)$. The set $E$ is nonempty, closed, and convex, and the point $(x_0,r_0)$ does not belong to $E$. By the finite-dimensional [strict separation theorem](/theorems/1044) for a point and a nonempty closed convex set (citing a result not yet in the wiki: finite-dimensional strict separation theorem), there exist $a_0 \in \mathbb{R}^n$, $\beta_0 \in \mathbb{R}$, and $\alpha_0 \in \mathbb{R}$ such that $(a_0,\beta_0) \neq (0,0)$ and \begin{align*} a_0 \cdot z + \beta_0 s \geq \alpha_0 > a_0 \cdot x_0 + \beta_0 r_0 \end{align*} for every $(z,s) \in E$. For any $z \in \operatorname{dom} f$ and any $t \geq 0$, the point $(z,f(z)+t)$ belongs to $E$. Hence \begin{align*} a_0 \cdot z + \beta_0 f(z) + \beta_0 t \geq \alpha_0 \end{align*} for every $t \geq 0$. This forces $\beta_0 \geq 0$. If $\beta_0=0$, then substituting $z=x_0$ gives \begin{align*} a_0 \cdot x_0 \geq \alpha_0 > a_0 \cdot x_0, \end{align*} a contradiction. Thus $\beta_0>0$. Define \begin{align*} y_0 := -\frac{a_0}{\beta_0} \in \mathbb{R}^n, \qquad c_0 := -\frac{\alpha_0}{\beta_0} \in \mathbb{R}. \end{align*} For every $z \in \operatorname{dom} f$, substituting $s=f(z)$ in the separation inequality gives \begin{align*} f(z) \geq z \cdot y_0 - c_0. \end{align*} For $z \notin \operatorname{dom} f$, the same inequality holds because $f(z)=+\infty$. Therefore the affine map \begin{align*} \ell_0: \mathbb{R}^n \to \mathbb{R}, \qquad \ell_0(z) := z \cdot y_0 - c_0 \end{align*} is a global affine minorant of $f$. In particular, \begin{align*} f^*(y_0) \leq c_0 < +\infty. \end{align*}[/step]

[guided]The purpose of this step is to guarantee that the epigraph has at least one genuine, finite affine supporting function below it. Since $f$ is proper, we may choose $x_0 \in \operatorname{dom} f$, so $f(x_0)$ is a real number. Choose $r_0 \in \mathbb{R}$ with $r_0 < f(x_0)$. Then the point $(x_0,r_0)$ lies strictly below the epigraph \begin{align*} E := \operatorname{epi} f = \{(z,s) \in \mathbb{R}^n \times \mathbb{R} : f(z) \leq s\}. \end{align*} Because $f$ is convex, $E$ is convex. Because $f$ is lower semicontinuous, $E$ is closed. Because $x_0 \in \operatorname{dom} f$, the point $(x_0,f(x_0))$ belongs to $E$, so $E$ is nonempty. We may therefore apply the finite-dimensional strict separation theorem for a point and a nonempty closed convex set (citing a result not yet in the wiki: finite-dimensional strict separation theorem). It gives coefficients $a_0 \in \mathbb{R}^n$, $\beta_0 \in \mathbb{R}$, and $\alpha_0 \in \mathbb{R}$, with $(a_0,\beta_0) \neq (0,0)$, such that \begin{align*} a_0 \cdot z + \beta_0 s \geq \alpha_0 > a_0 \cdot x_0 + \beta_0 r_0 \end{align*} for every $(z,s) \in E$. Now we use the special geometry of an epigraph. If $z \in \operatorname{dom} f$ and $t \geq 0$, then $(z,f(z)+t) \in E$. Substituting this point into the separating inequality gives \begin{align*} a_0 \cdot z + \beta_0 f(z) + \beta_0 t \geq \alpha_0 \end{align*} for every $t \geq 0$. This is impossible when $\beta_0<0$, since the left-hand side tends to $-\infty$ as $t \to +\infty$. Hence $\beta_0 \geq 0$. We also need $\beta_0$ to be strictly positive, because only then can we solve the inequality for $f(z)$. If $\beta_0=0$, then applying the separating inequality to $(x_0,f(x_0)) \in E$ gives $a_0 \cdot x_0 \geq \alpha_0$, while the strict inequality gives $\alpha_0 > a_0 \cdot x_0$. This contradiction proves $\beta_0>0$. Since $\beta_0>0$, define \begin{align*} y_0 := -\frac{a_0}{\beta_0} \in \mathbb{R}^n, \qquad c_0 := -\frac{\alpha_0}{\beta_0} \in \mathbb{R}. \end{align*} For $z \in \operatorname{dom} f$, substituting $s=f(z)$ into the separation inequality and dividing by $\beta_0$ gives \begin{align*} f(z) \geq z \cdot y_0 - c_0. \end{align*} For $z \notin \operatorname{dom} f$, we have $f(z)=+\infty$, so the same inequality is automatic. Therefore \begin{align*} \ell_0: \mathbb{R}^n \to \mathbb{R}, \qquad \ell_0(z) := z \cdot y_0 - c_0 \end{align*} is a global affine minorant of $f$. Equivalently, $z \cdot y_0 - f(z) \leq c_0$ for every $z \in \mathbb{R}^n$, and hence \begin{align*} f^*(y_0) \leq c_0 < +\infty. \end{align*}[/guided]

[step:Separate an arbitrary point below the epigraph] Fix $x \in \mathbb{R}^n$ and fix $r \in \mathbb{R}$ with $r < f(x)$. Then $(x,r) \notin E$. Applying again the finite-dimensional strict separation theorem for a point and a nonempty closed convex set (citing a result not yet in the wiki: finite-dimensional strict separation theorem), choose $a \in \mathbb{R}^n$, $\beta \in \mathbb{R}$, and $\alpha \in \mathbb{R}$ with $(a,\beta)\neq(0,0)$ such that \begin{align*} a \cdot z + \beta s \geq \alpha > a \cdot x + \beta r \end{align*} for every $(z,s) \in E$. As before, the vertical-ray property of $E$ forces $\beta \geq 0$. [/step]

[step:Handle the nonvertical separation by producing a finite conjugate slope] Assume first that $\beta>0$. Define \begin{align*} y := -\frac{a}{\beta} \in \mathbb{R}^n, \qquad c := -\frac{\alpha}{\beta} \in \mathbb{R}. \end{align*} For every $z \in \operatorname{dom} f$, substituting $s=f(z)$ in the separation inequality gives \begin{align*} f(z) \geq z \cdot y - c. \end{align*} For $z \notin \operatorname{dom} f$, this inequality is automatic because $f(z)=+\infty$. Therefore \begin{align*} f^*(y) = \sup_{z \in \mathbb{R}^n} \{z \cdot y - f(z)\} \leq c < +\infty. \end{align*} The strict separation at $(x,r)$ gives \begin{align*} x \cdot y - c > r. \end{align*} Since $f^*(y) \leq c$, we obtain \begin{align*} f^{**}(x) \geq x \cdot y - f^*(y) \geq x \cdot y - c > r. \end{align*} [/step]

[step:Handle the horizontal separation by tilting a fixed affine minorant]Assume now that $\beta=0$. Then the separation inequality says \begin{align*} a \cdot z \geq \alpha > a \cdot x \end{align*} for every $z \in \operatorname{dom} f$. Let $\lambda>0$. Define \begin{align*} y_\lambda := y_0 - \lambda a \in \mathbb{R}^n, \qquad c_\lambda := c_0 - \lambda \alpha \in \mathbb{R}, \end{align*} and define the affine map \begin{align*} \ell_\lambda: \mathbb{R}^n \to \mathbb{R}, \qquad \ell_\lambda(z) := z \cdot y_\lambda - c_\lambda. \end{align*} Equivalently, \begin{align*} \ell_\lambda(z) = \ell_0(z) - \lambda(a \cdot z-\alpha). \end{align*} For $z \in \operatorname{dom} f$, the inequality $a \cdot z-\alpha \geq 0$ gives \begin{align*} \ell_\lambda(z) \leq \ell_0(z) \leq f(z). \end{align*} For $z \notin \operatorname{dom} f$, the inequality is automatic because $f(z)=+\infty$. Thus $\ell_\lambda$ is a global affine minorant of $f$, so \begin{align*} f^*(y_\lambda) \leq c_\lambda < +\infty. \end{align*} At the fixed point $x$, \begin{align*} \ell_\lambda(x) = \ell_0(x) + \lambda(\alpha-a \cdot x). \end{align*} Since $\alpha-a \cdot x>0$, choose $\lambda>0$ large enough that $\ell_\lambda(x)>r$. Then \begin{align*} f^{**}(x) \geq x \cdot y_\lambda - f^*(y_\lambda) \geq x \cdot y_\lambda - c_\lambda = \ell_\lambda(x) > r. \end{align*}[/step]

[guided]The horizontal case is the subtle part. The separation has $\beta=0$, so it does not directly solve for a lower bound on $f(z)$. Instead, it tells us that the whole effective domain of $f$ lies on one side of the hyperplane $a \cdot z=\alpha$, while the point $x$ lies strictly on the other side: \begin{align*} a \cdot z \geq \alpha > a \cdot x \end{align*} for every $z \in \operatorname{dom} f$. A horizontal separator alone is not an affine minorant of $f$. The remedy is to start from the affine minorant already constructed: \begin{align*} \ell_0: \mathbb{R}^n \to \mathbb{R}, \qquad \ell_0(z) := z \cdot y_0 - c_0, \end{align*} where $\ell_0(z) \leq f(z)$ for every $z \in \mathbb{R}^n$. For each $\lambda>0$, define \begin{align*} y_\lambda := y_0 - \lambda a \in \mathbb{R}^n, \qquad c_\lambda := c_0 - \lambda \alpha \in \mathbb{R}, \end{align*} and \begin{align*} \ell_\lambda: \mathbb{R}^n \to \mathbb{R}, \qquad \ell_\lambda(z) := z \cdot y_\lambda - c_\lambda. \end{align*} This is the same as \begin{align*} \ell_\lambda(z) = \ell_0(z) - \lambda(a \cdot z-\alpha). \end{align*} Why does this remain below $f$? If $z \in \operatorname{dom} f$, then the horizontal separation gives $a \cdot z-\alpha \geq 0$, so subtracting $\lambda(a \cdot z-\alpha)$ can only decrease $\ell_0(z)$. Hence \begin{align*} \ell_\lambda(z) \leq \ell_0(z) \leq f(z). \end{align*} If $z \notin \operatorname{dom} f$, then $f(z)=+\infty$, so the inequality $\ell_\lambda(z)\leq f(z)$ is automatic. Thus $\ell_\lambda$ is a global affine minorant of $f$. Writing $\ell_\lambda(z)=z \cdot y_\lambda-c_\lambda$, the minorant inequality gives \begin{align*} z \cdot y_\lambda - f(z) \leq c_\lambda \end{align*} for every $z \in \mathbb{R}^n$. Taking the supremum over $z$ proves \begin{align*} f^*(y_\lambda) \leq c_\lambda < +\infty. \end{align*} So the affine function $\ell_\lambda$ is one of the finite conjugate affine functions contributing to $f^{**}$. At the separated point $x$, the sign reverses in our favor: \begin{align*} \ell_\lambda(x) = \ell_0(x) + \lambda(\alpha-a \cdot x). \end{align*} Since $\alpha-a \cdot x>0$, this value tends to $+\infty$ as $\lambda \to +\infty$. Therefore we may choose $\lambda>0$ such that $\ell_\lambda(x)>r$. For this choice, \begin{align*} f^{**}(x) \geq x \cdot y_\lambda - f^*(y_\lambda) \geq x \cdot y_\lambda - c_\lambda = \ell_\lambda(x) > r. \end{align*} This proves that even a horizontal separator yields finite conjugate slopes whose affine values at $x$ exceed the prescribed level $r$.[/guided]

[step:Recover $f$ from its finite affine minorants] We have proved that for every $x \in \mathbb{R}^n$ and every $r \in \mathbb{R}$ with $r<f(x)$, \begin{align*} f^{**}(x) > r. \end{align*} If $f(x)<+\infty$, letting $r \uparrow f(x)$ gives $f^{**}(x)\geq f(x)$. Combined with $f^{**}(x)\leq f(x)$, this gives $f^{**}(x)=f(x)$. If $f(x)=+\infty$, then the preceding inequality holds for every real $r$, so $f^{**}(x)=+\infty=f(x)$. Hence $f=f^{**}$ whenever $f$ is convex and lower semicontinuous. [/step]

[step:Derive convexity and lower semicontinuity from equality] Conversely, suppose $f=f^{**}$. Since $f^{**}$ is convex and lower semicontinuous by the supremum representation above, $f$ is convex and lower semicontinuous. Because the original $f$ is proper and takes values in $(-\infty,+\infty]$, equality also implies that $f^{**}$ is proper and never takes the value $-\infty$. [/step]

[step:Identify the affine-support reconstruction in the equality case] Assume $f=f^{**}$. Let \begin{align*} \mathcal{A} := \{(y,c) \in \mathbb{R}^n \times \mathbb{R} : z \cdot y - c \leq f(z) \text{ for every } z \in \mathbb{R}^n\}. \end{align*} For a pair $(y,c) \in \mathbb{R}^n \times \mathbb{R}$, the condition $(y,c)\in\mathcal{A}$ is equivalent to \begin{align*} f^*(y) \leq c. \end{align*} Therefore every affine minorant $z \mapsto z \cdot y-c$ contributes a value no larger than $z \mapsto z \cdot y-f^*(y)$, and conversely $z \mapsto z \cdot y-f^*(y)$ is itself an affine minorant whenever $f^*(y)<+\infty$. Hence for every $x \in \mathbb{R}^n$, \begin{align*} f(x) = f^{**}(x) = \sup_{y \in \mathbb{R}^n} \{x \cdot y - f^*(y)\} = \sup_{(y,c)\in\mathcal{A}} \{x \cdot y-c\}. \end{align*} This is precisely the stated finite affine-support reconstruction. [/step]