[proofplan]
The proof is an order-theoretic calculation from the definition of the $c$-transform. First, the defining infimum for $\varphi^c$ gives a pointwise inequality against every competitor $x \in X$, and rearranging this inequality gives $\varphi \leq \varphi^{cc}$. For the reverse inequality under $c$-concavity, write $\varphi=\psi^c$, apply the same general inequality to $\psi$, and then use the fact that the $c$-transform reverses pointwise order, proved directly from the defining infimum.
[/proofplan]
[step:Record the extended-real subtraction rules used below]
We use the following elementary rules for extended-real subtraction, always only when the displayed differences are defined. First, if $a,b,d \in [-\infty,\infty]$, $d \leq a-b$, and both $a-b$ and $a-d$ are defined, then
\begin{align*}
b \leq a-d.
\end{align*}
To prove this, consider the value of $a$. If $a\in\mathbb{R}$ and $b\in\mathbb{R}$, then $d\leq a-b$ gives $b\leq a-d$ by ordinary real subtraction, with the endpoint cases $d=\infty$ and $d=-\infty$ giving respectively an impossible hypothesis and the conclusion $b\leq\infty$. If $a\in\mathbb{R}$ and $b=\infty$, then $a-b=-\infty$, so $d=-\infty$ and $a-d=\infty$, hence $b\leq a-d$. If $a\in\mathbb{R}$ and $b=-\infty$, then $a-b=\infty$, while the definedness of $a-d$ excludes no value of $d$ except none of the real-endpoint cases; in every permitted case $a-d\in[-\infty,\infty]$ and $b=-\infty\leq a-d$. If $a=\infty$, the definedness of $a-b$ and $a-d$ gives $b<\infty$ and $d<\infty$, so $a-d=\infty$ and therefore $b\leq a-d$. If $a=-\infty$, the definedness of $a-b$ gives $b>-\infty$. The inequality $d\leq a-b$ forces $d=-\infty$ whenever $b<\infty$, making $a-d$ undefined; if $b=\infty$, then $a-b=-\infty$ again forces $d=-\infty$, also making $a-d$ undefined. Thus the case $a=-\infty$ cannot occur under the stated hypotheses.
Second, if $a,b_1,b_2 \in [-\infty,\infty]$, $b_1\leq b_2$, and both $a-b_1$ and $a-b_2$ are defined, then
\begin{align*}
a-b_2 \leq a-b_1.
\end{align*}
For $a\in\mathbb{R}$ this is the ordinary order-reversal of subtraction, including the endpoint cases. For $a=\infty$, definedness forces $b_1,b_2<\infty$, and the conclusion follows because both differences are either ordinary finite subtractions or equal to $\infty$ at the endpoint $b_i=-\infty$. For $a=-\infty$, definedness forces $b_1,b_2>-\infty$, and both differences are either ordinary finite subtractions or equal to $-\infty$ at the endpoint $b_i=\infty$.
[/step]
[step:Use the defining infimum to prove $\varphi \leq \varphi^{cc}$]
Fix $x_0 \in X$ and $y \in Y$. Define the function
\begin{align*}
A_y:X &\to [-\infty,\infty]
\end{align*}
\begin{align*}
x &\mapsto c(x,y)-\varphi(x).
\end{align*}
By definition of the infimum,
\begin{align*}
\varphi^c(y)=\inf_{x \in X} A_y(x) \leq A_y(x_0)=c(x_0,y)-\varphi(x_0).
\end{align*}
Since the extended-real differences $c(x_0,y)-\varphi(x_0)$ and $c(x_0,y)-\varphi^c(y)$ are defined by hypothesis, the first extended-real subtraction rule applies with
\begin{align*}
a=c(x_0,y), \qquad b=\varphi(x_0), \qquad d=\varphi^c(y).
\end{align*}
It gives
\begin{align*}
\varphi(x_0) \leq c(x_0,y)-\varphi^c(y).
\end{align*}
The point $y \in Y$ was arbitrary, so $\varphi(x_0)$ is a lower bound for the set
\begin{align*}
\{c(x_0,y)-\varphi^c(y):y \in Y\}.
\end{align*}
Taking the infimum over $y \in Y$ gives
\begin{align*}
\varphi(x_0) \leq \inf_{y \in Y}\bigl(c(x_0,y)-\varphi^c(y)\bigr)=\varphi^{cc}(x_0).
\end{align*}
Since $x_0 \in X$ was arbitrary, $\varphi \leq \varphi^{cc}$ pointwise on $X$.
[guided]
Fix $x_0 \in X$. We want to compare $\varphi(x_0)$ with $\varphi^{cc}(x_0)$, whose definition is an infimum over $Y$. Therefore the right way to prove $\varphi(x_0)\leq \varphi^{cc}(x_0)$ is to prove that $\varphi(x_0)$ is below every term appearing in that infimum.
For a fixed $y \in Y$, define
\begin{align*}
A_y:X &\to [-\infty,\infty]
\end{align*}
\begin{align*}
x &\mapsto c(x,y)-\varphi(x).
\end{align*}
The $c$-transform is exactly the infimum of this function:
\begin{align*}
\varphi^c(y)=\inf_{x \in X} A_y(x).
\end{align*}
An infimum is bounded above by every value of the function, so evaluating at the specific point $x_0$ gives
\begin{align*}
\varphi^c(y) \leq A_y(x_0)=c(x_0,y)-\varphi(x_0).
\end{align*}
The hypotheses exclude the undefined extended-real expressions needed here, namely $c(x_0,y)-\varphi(x_0)$ and $c(x_0,y)-\varphi^c(y)$. Therefore we may use the extended-real subtraction rule proved above: if $d\leq a-b$ and both $a-b$ and $a-d$ are defined, then $b\leq a-d$. Applying it with
\begin{align*}
a=c(x_0,y), \qquad b=\varphi(x_0), \qquad d=\varphi^c(y)
\end{align*}
gives
\begin{align*}
\varphi(x_0) \leq c(x_0,y)-\varphi^c(y).
\end{align*}
This holds for every $y \in Y$. Thus $\varphi(x_0)$ is a lower bound for all numbers of the form $c(x_0,y)-\varphi^c(y)$. Taking the infimum over $y$ preserves that lower-bound inequality:
\begin{align*}
\varphi(x_0) \leq \inf_{y \in Y}\bigl(c(x_0,y)-\varphi^c(y)\bigr).
\end{align*}
By the definition of the second $c$-transform,
\begin{align*}
\inf_{y \in Y}\bigl(c(x_0,y)-\varphi^c(y)\bigr)=\varphi^{cc}(x_0).
\end{align*}
Therefore $\varphi(x_0)\leq \varphi^{cc}(x_0)$. Since $x_0$ was arbitrary, $\varphi \leq \varphi^{cc}$ on $X$.
[/guided]
[/step]
[step:Prove directly that the $c$-transform reverses pointwise order]
Let $\alpha,\beta:Y \to [-\infty,\infty]$ be functions such that $\alpha(y)\leq \beta(y)$ for every $y \in Y$, and assume the expressions defining $\alpha^c$ and $\beta^c$ are defined. Fix $x \in X$. For every $y \in Y$, the differences $c(x,y)-\alpha(y)$ and $c(x,y)-\beta(y)$ are defined by the assumed well-definedness of the two transforms. The second extended-real subtraction rule applies with
\begin{align*}
a=c(x,y), \qquad b_1=\alpha(y), \qquad b_2=\beta(y),
\end{align*}
and gives
\begin{align*}
c(x,y)-\beta(y) \leq c(x,y)-\alpha(y).
\end{align*}
Taking infima over $y \in Y$ gives
\begin{align*}
\beta^c(x)=\inf_{y \in Y}\bigl(c(x,y)-\beta(y)\bigr) \leq \inf_{y \in Y}\bigl(c(x,y)-\alpha(y)\bigr)=\alpha^c(x).
\end{align*}
Thus $\beta^c \leq \alpha^c$ pointwise on $X$.
[guided]
The $c$-transform reverses order because the variable function is subtracted from the fixed cost. Let $\alpha,\beta:Y \to [-\infty,\infty]$ satisfy $\alpha(y)\leq\beta(y)$ for every $y\in Y$, and assume that for every $x\in X$ and $y\in Y$ both differences $c(x,y)-\alpha(y)$ and $c(x,y)-\beta(y)$ are defined. Fix $x\in X$ and $y\in Y$. Applying the second extended-real subtraction rule with
\begin{align*}
a=c(x,y), \qquad b_1=\alpha(y), \qquad b_2=\beta(y)
\end{align*}
gives
\begin{align*}
c(x,y)-\beta(y) \leq c(x,y)-\alpha(y).
\end{align*}
This is the pointwise inequality between the two functions of $y$ whose infima define $\beta^c(x)$ and $\alpha^c(x)$. Since the infimum is monotone with respect to pointwise order of functions, taking the infimum over $Y$ yields
\begin{align*}
\inf_{y \in Y}\bigl(c(x,y)-\beta(y)\bigr) \leq \inf_{y \in Y}\bigl(c(x,y)-\alpha(y)\bigr).
\end{align*}
By the definition of the two $c$-transforms, this is exactly
\begin{align*}
\beta^c(x) \leq \alpha^c(x).
\end{align*}
Because $x\in X$ was arbitrary, $\beta^c\leq\alpha^c$ pointwise on $X$.
[/guided]
[/step]
[step:Use $c$-concavity to obtain the reverse inequality]
Assume now that $\varphi$ is $c$-concave. Then there exists a function $\psi:Y \to [-\infty,\infty]$ such that
\begin{align*}
\varphi=\psi^c.
\end{align*}
By the explicit $c$-concavity hypothesis in the theorem statement, for every $x\in X$ and $y\in Y$ the differences $c(x,y)-\psi(y)$, $c(x,y)-\psi^c(x)$, and $c(x,y)-\psi^{cc}(y)$ are defined. The first two families of differences are exactly the hypotheses needed to apply the [first inequality](/theorems/2897) to $\psi$, with the roles of $X$ and $Y$ interchanged. This gives
\begin{align*}
\psi \leq \psi^{cc}.
\end{align*}
The second and third families of differences are exactly the hypotheses needed to apply the order-reversing property to the pointwise inequality $\psi\leq\psi^{cc}$. Therefore
\begin{align*}
(\psi^{cc})^c \leq \psi^c.
\end{align*}
Since $\varphi=\psi^c$, we have $\psi^{cc}=(\psi^c)^c=\varphi^c$, and therefore
\begin{align*}
(\psi^{cc})^c=(\varphi^c)^c=\varphi^{cc}.
\end{align*}
Hence
\begin{align*}
\varphi^{cc}\leq \varphi.
\end{align*}
Combining this with the already proved inequality $\varphi \leq \varphi^{cc}$ yields
\begin{align*}
\varphi^{cc}=\varphi.
\end{align*}
This proves the involution identity for $c$-concave functions.
[/step]