[proofplan]
The proof is an order-duality argument between sublevel inequalities and containment in dilates of polar sets. First we show that membership $y \in \lambda K^\circ$ is exactly the same as the inequality $x \cdot y \leq \lambda$ for all $x \in K$, and taking the infimum over such $\lambda$ gives $p_{K^\circ}(y)=h_K(y)$. For the reverse identity, we use the same argument after identifying the bipolar $(K^\circ)^\circ$ with $K$; the needed bipolar fact follows from the finite-dimensional separating hyperplane theorem because $K$ is closed, convex, and contains $0$.
[/proofplan]
[step:Translate membership in a polar dilate into support inequalities]
Fix $y \in \mathbb{R}^n$ with $p_{K^\circ}(y)<\infty$. For each $\lambda>0$, the definition of scalar multiplication gives
\begin{align*}
y \in \lambda K^\circ
\iff
\frac{y}{\lambda} \in K^\circ.
\end{align*}
By the definition of $K^\circ$, this is equivalent to
\begin{align*}
x \cdot \frac{y}{\lambda} \leq 1
\quad \text{for every } x \in K,
\end{align*}
and hence to
\begin{align*}
x \cdot y \leq \lambda
\quad \text{for every } x \in K.
\end{align*}
Therefore
\begin{align*}
\{\lambda>0 : y \in \lambda K^\circ\}
=
\{\lambda>0 : h_K(y) \leq \lambda\}.
\end{align*}
[guided]
We first unpack the two definitions without changing any geometry. Fix $y \in \mathbb{R}^n$ and let $\lambda>0$. Since $\lambda K^\circ=\{\lambda z:z\in K^\circ\}$, the condition $y\in\lambda K^\circ$ is equivalent to $\lambda^{-1}y\in K^\circ$.
Now apply the definition of the polar set. The statement $\lambda^{-1}y\in K^\circ$ means exactly that every point $x\in K$ satisfies
\begin{align*}
x\cdot \frac{y}{\lambda}\leq 1.
\end{align*}
Because $\lambda>0$, multiplying by $\lambda$ preserves the inequality and gives
\begin{align*}
x\cdot y\leq \lambda
\quad \text{for every } x\in K.
\end{align*}
Taking the supremum over $x\in K$ is precisely the support function:
\begin{align*}
h_K(y)=\sup_{x\in K}x\cdot y.
\end{align*}
Thus $y\in\lambda K^\circ$ holds exactly for those positive $\lambda$ that dominate $h_K(y)$:
\begin{align*}
\{\lambda>0:y\in\lambda K^\circ\}
=
\{\lambda>0:h_K(y)\leq\lambda\}.
\end{align*}
[/guided]
[/step]
[step:Take the infimum to identify $h_K$ with $p_{K^\circ}$]
By definition of the gauge,
\begin{align*}
p_{K^\circ}(y)
=
\inf\{\lambda>0 : y \in \lambda K^\circ\}.
\end{align*}
Using the equality of sets from the previous step,
\begin{align*}
p_{K^\circ}(y)
=
\inf\{\lambda>0 : h_K(y)\leq \lambda\}.
\end{align*}
Since $p_{K^\circ}(y)<\infty$, this set is nonempty. The equality also implies that $h_K(y)<\infty$: if some $\lambda>0$ satisfies $h_K(y)\leq\lambda$, then $h_K(y)$ is finite. Hence
\begin{align*}
\inf\{\lambda>0 : h_K(y)\leq \lambda\}
=
h_K(y),
\end{align*}
and therefore
\begin{align*}
p_{K^\circ}(y)=h_K(y).
\end{align*}
[guided]
The gauge of $K^\circ$ is defined by searching over all positive dilates of $K^\circ$ that contain $y$:
\begin{align*}
p_{K^\circ}(y)
=
\inf\{\lambda>0:y\in\lambda K^\circ\}.
\end{align*}
The previous step converted this containment condition into the scalar inequality $h_K(y)\leq \lambda$. Therefore
\begin{align*}
p_{K^\circ}(y)
=
\inf\{\lambda>0:h_K(y)\leq \lambda\}.
\end{align*}
Because $p_{K^\circ}(y)<\infty$, there exists at least one $\lambda>0$ with $y\in\lambda K^\circ$, and hence at least one $\lambda>0$ with $h_K(y)\leq\lambda$. Thus $h_K(y)$ is finite. For a finite real number $a$, the infimum of all positive $\lambda$ satisfying $a\leq\lambda$ is $a$ when such positive upper bounds exist and $a\geq0$; here $a=h_K(y)\geq0$ because $0\in K$ gives $h_K(y)\geq 0\cdot y=0$. Hence
\begin{align*}
\inf\{\lambda>0:h_K(y)\leq \lambda\}
=
h_K(y).
\end{align*}
Thus
\begin{align*}
p_{K^\circ}(y)=h_K(y).
\end{align*}
[/guided]
[/step]
[step:Identify the bipolar of $K$ with $K$]
We record the finite-dimensional bipolar fact needed for the second identity:
\begin{align*}
(K^\circ)^\circ=K.
\end{align*}
Indeed, if $x\in K$, then for every $y\in K^\circ$ one has $x\cdot y\leq1$, so $x\in(K^\circ)^\circ$.
Conversely, suppose $x\notin K$. Since $K$ is closed and convex, the finite-dimensional [strict separation theorem](/theorems/1044) gives a vector $y\in\mathbb{R}^n$ and a real number $\alpha\in\mathbb{R}$ such that
\begin{align*}
z\cdot y\leq \alpha < x\cdot y
\quad \text{for every } z\in K.
\end{align*}
Because $0\in K$, the inequality with $z=0$ gives $0\leq \alpha$. Since $\alpha < x\cdot y$, we have $x\cdot y>0$. Choose a scalar $c>0$ such that
\begin{align*}
c\alpha \leq 1
\quad \text{and} \quad
c\,x\cdot y>1.
\end{align*}
Then $cy\in K^\circ$ because $z\cdot(cy)\leq c\alpha\leq1$ for every $z\in K$, while $x\cdot(cy)>1$. Hence $x\notin(K^\circ)^\circ$. Therefore $(K^\circ)^\circ=K$.
[guided]
We need to justify why applying the first identity to $K^\circ$ will return $K$, rather than a larger set. This is the bipolar statement:
\begin{align*}
(K^\circ)^\circ=K.
\end{align*}
First, $K\subset (K^\circ)^\circ$. If $x\in K$ and $y\in K^\circ$, then the definition of $K^\circ$ gives
\begin{align*}
x\cdot y\leq1.
\end{align*}
Since this holds for every $y\in K^\circ$, the definition of the polar of $K^\circ$ gives $x\in(K^\circ)^\circ$.
For the reverse inclusion, let $x\in\mathbb{R}^n\setminus K$. The set $K$ is closed and convex, so the finite-dimensional strict separation theorem gives a vector $y\in\mathbb{R}^n$ and a real number $\alpha\in\mathbb{R}$ such that
\begin{align*}
z\cdot y\leq \alpha < x\cdot y
\quad \text{for every } z\in K.
\end{align*}
The hypothesis $0\in K$ is used here to control the sign of the separating level: substituting $z=0$ gives $0\leq\alpha$. Since $\alpha<x\cdot y$, this also gives $x\cdot y>0$.
We now rescale the separating vector so that it becomes an element of $K^\circ$ while still detecting that $x$ is outside the bipolar. Choose $c>0$ satisfying
\begin{align*}
c\alpha\leq1
\quad \text{and}\quad
c\,x\cdot y>1.
\end{align*}
Such a choice is possible because $\alpha<x\cdot y$ and $x\cdot y>0$. For every $z\in K$ we then have
\begin{align*}
z\cdot(cy)=c(z\cdot y)\leq c\alpha\leq1,
\end{align*}
so $cy\in K^\circ$. But
\begin{align*}
x\cdot(cy)>1,
\end{align*}
which means $x\notin(K^\circ)^\circ$. Thus every point outside $K$ is outside $(K^\circ)^\circ$, and therefore
\begin{align*}
(K^\circ)^\circ=K.
\end{align*}
[/guided]
[/step]
[step:Apply the first identity to the polar set]
The set $K^\circ$ is nonempty, closed, convex, and contains $0$: nonemptiness and $0\in K^\circ$ follow from $0\cdot z=0\leq1$ for every $z\in K$; convexity and closedness follow because
\begin{align*}
K^\circ=\bigcap_{z\in K}\{w\in\mathbb{R}^n:z\cdot w\leq1\},
\end{align*}
an intersection of closed half-spaces.
Applying the first identity, already proved, with $K^\circ$ in place of $K$, gives, for every $x\in\mathbb{R}^n$ with $p_{(K^\circ)^\circ}(x)<\infty$,
\begin{align*}
h_{K^\circ}(x)=p_{(K^\circ)^\circ}(x).
\end{align*}
Using $(K^\circ)^\circ=K$, this becomes
\begin{align*}
h_{K^\circ}(x)=p_K(x)
\end{align*}
for every $x\in\mathbb{R}^n$ with $p_K(x)<\infty$.
[guided]
We now repeat the first part of the proof with $K^\circ$ as the set in place of $K$. To do that, we verify the structural hypotheses for $K^\circ$.
First, $0\in K^\circ$ because for every $z\in K$,
\begin{align*}
z\cdot0=0\leq1.
\end{align*}
Second, $K^\circ$ is convex and closed because it is the intersection of the closed half-spaces
\begin{align*}
\{w\in\mathbb{R}^n:z\cdot w\leq1\},
\end{align*}
indexed by $z\in K$:
\begin{align*}
K^\circ=\bigcap_{z\in K}\{w\in\mathbb{R}^n:z\cdot w\leq1\}.
\end{align*}
The first identity proved above therefore applies to $K^\circ$. For every $x\in\mathbb{R}^n$ such that $p_{(K^\circ)^\circ}(x)<\infty$, it gives
\begin{align*}
h_{K^\circ}(x)=p_{(K^\circ)^\circ}(x).
\end{align*}
The bipolar step identifies $(K^\circ)^\circ$ with $K$, so
\begin{align*}
p_{(K^\circ)^\circ}(x)=p_K(x).
\end{align*}
Thus, for every $x\in\mathbb{R}^n$ with $p_K(x)<\infty$,
\begin{align*}
h_{K^\circ}(x)=p_K(x).
\end{align*}
[/guided]
[/step]