From c81b77a721e4274457ebee2d0fd0ed21f4334bb9 Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Wed, 24 Jun 2026 22:06:22 -0400
Subject: [PATCH] Added the separable corollary to the Legendre transform.

---
 src/fa/convex/legendre.tex | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/fa/convex/legendre.tex b/src/fa/convex/legendre.tex
index 5daaff1..f3b6de0 100644
--- a/src/fa/convex/legendre.tex
+++ b/src/fa/convex/legendre.tex
@@ -217,5 +217,28 @@
     By \autoref{lemma:conjugate-function-gymnatics}, $f^{**}$ is lower semicontinuous and convex with so $f^{**} \le f$, so $\text{epi}(f^{**}) \supset \text{epi}(f)$ and $\text{epi}(f^{**}) \supset \ol{\text{Conv}}(\text{epi}(f))$.    
 \end{proof}
 
+\begin{corollary}
+\label{corollary:separable-legendre}
+    Let $\dpn{E, F}{\lambda}$ be a duality over $\real$, and $f: E \to (-\infty, \infty]$ with $f \ne \infty$ be convex and lower semicontinuous, then there exists $\seq{(\phi_n, \alpha_n)} \subset F \times \real$ such that for each $x \in E$, 
+    \[
+    f(x) = \sup_{n \in \natp} \dpn{x, \phi_n}{\lambda} - \alpha_n
+    \]
+\end{corollary}
+\begin{proof}
+    For each $(\phi, \alpha) \in F \times \real$, denote $(\phi, \alpha) \le f$ if $\dpn{\cdot, \phi}{\lambda} - \alpha \le f$. By the \hyperref[Fenchel-Moreau Theorem]{theorem:fenchel-moreau},  
+    \[
+    f^{**}(x) = \sup\bracs{\dpn{x, \phi}{\lambda} - \alpha|(\phi, \alpha) \in F \times \real, (\phi, \alpha) \le f}
+    \]
+
+    for all $x \in E$. By \autoref{proposition:separable-dual},
+    \[
+    S = \bracs{(\phi, \alpha) \in F \times \real| (\phi, \alpha) \le f}
+    \]
+
+    is separable with respect to $\sigma(F \times \real, E \times \real)$. Therefore there exists $\seq{(\phi_n, \alpha_n)} \subset S$ such that for each $x \in E$, 
+    \[
+    f(x) = \sup_{n \in \natp} \dpn{x, \phi_n}{\lambda} - \alpha_n
+    \]
+\end{proof}