Theorem: Ekeland's Variational Principle

Let $\struct {X, d}$ be a complete metric space.
Let $\phi : X \to \R \cup \set \infty$ be a lower semicontinuous function that is bounded below.
Then for each $\epsilon > 0$, there exists $x_0 \in X$ such that:
:$\map \phi x \ge \map \phi {x_0} - \epsilon \map d {x, x_0}$ for each $x \in X$.

Proof:
Take $M \in \N$ such that:
:$\map \phi x \ge M$ for each $x \in X$. 
Then, for any $y \in X$, we have:
:$\map \phi x + \map d {x, y} \ge M$
Hence, for each $y \in X$:
:$\inf \set {\map \phi x + \map d {x, y} : x \in X}$ is finite. 
Fix any $y_1 \in X$.
We construct a sequence $\sequence {y_n}_{n \mathop \in \N}$ inductively. 
Given $y_n \in X$, take $y_{n + 1} \in X$ to be such that:
:$\ds \map \phi {y_{n + 1} } + \epsilon \map d {y_n, y_{n + 1} } \le \inf \set {\map \phi x + \map d {x, y_n} : x \in X} + \frac 1 {2^n}$
With that, we have:
:$\ds \map \phi {y_{n + 1} } + \epsilon \map d {y_n, y_{n + 1} } \le \map \phi {y_n} + \map d {y_n, y_n} + \frac 1 {2^n} = \map \phi {y_n} + \frac 1 {2^n}$ 
Hence:
:$\ds \map \phi {y_{n + 1} } \le \map \phi {y_{n + 1} } + \epsilon \map d {y_n, y_{n + 1} } \le \map \phi {y_n} + \frac 1 {2^n}$
Hence:
:$\map \phi {y_{n + 1} } + 2^{-n} \le \map \phi {y_n} + 2 \times 2^{-n} = \map \phi {y_n} + 2^{1 - n}$ for each $n \in \N$. 
Noting that:
:$2^{-n} = 2^{1 - \paren {n + 1} }$
we see that $\sequence {\map \phi {y_n} + 2^{1 - n} }_{n \mathop \in \N}$ is a decreasing sequence.
We further have:
:$\map \phi {y_n} + 2^{1 - n} \ge M$ for each $n \in \N$.
From Monotone Convergence Theorem (Real Analysis): Decreasing Sequence, we have that:
:$\sequence {\map \phi {y_n} + 2^{1 - n} }_{n \mathop \in \N}$ converges to some $z \in \R$.
From Sum Rule for Real Sequences, we therefore have:
:$\map \phi {y_n} \to z$ as $n \to \infty$.
We aim to deduce that $\sequence {y_n}_{n \mathop \in \N}$ converges.
We have that:
:$\ds \epsilon \map d {y_n, y_{n + 1} } \le \map \phi {y_n} - \map \phi {y_{n + 1} } + \frac 1 {2^n}$
From Telescoping Series: Example 1, we have:
:$\ds \sum_{n \mathop = 1}^\infty \paren {\map \phi {y_n} - \map \phi {y_{n + 1} } } = \map \phi {y_1}$ 
From Sum of Infinite Geometric Sequence, we have:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 {2^n} = 1$
Hence we have:
:$\ds \sum_{n \mathop = 1}^\infty \map d {y_n, y_{n + 1} } \le \epsilon^{-1} \paren {\map \phi {y_1} + 1} < \infty$
Hence from Sequence in Metric Space with Summable Difference between Consecutive Terms is Cauchy Sequence: Corollary:
:$\sequence {y_n}_{n \mathop \in \N}$ converges to some $x_0 \in X$. 
By the choice of $y_{n + 1}$, we have:
:$\map \phi {y_{n + 1} } \le \map \phi x + \epsilon \map d {x, y_n} + 2^{-n} - \map d {y_{n + 1}, y_n}$
From Relationship between Limit Inferior and Lower Limit, we have:
:$\ds \liminf_{y \mathop \to x_0} \map \phi y \le \liminf_{n \mathop \to \infty} \map \phi {y_{n + 1} }$
We have:
:$\ds \liminf_{n \mathop \to \infty} \map \phi {y_{n + 1} } \le \liminf_{n \mathop \to \infty} \paren {\map \phi x + \epsilon \map d {x, y_n} + 2^{-n} - \map d {y_{n + 1}, y_n} }$
Since:
:$\ds \sum_{n \mathop = 1}^\infty \map d {y_{n + 1}, y_n} < \infty$
we have:
:$\map d {y_{n + 1}, y_n} \to 0$ as $n \to \infty$
from Terms in Convergent Series Converge to Zero.
From Distance Function of Metric Space is Continuous and Vertical Section of Continuous Function is Continuous, we have that:
:$\map d {x, y_n} \to \map d {x, x_0}$ as $n \to \infty$.
From Convergence of Limsup and Liminf, we have:
:$\ds \liminf_{n \mathop \to \infty} \paren {\map \phi x + \epsilon \map d {x, y_n} + 2^{-n} - \map d {y_{n + 1}, y_n} } = \map \phi x + \epsilon \map d {x, x_0}$
Hence:
:$\ds \liminf_{y \mathop \to x_0} \map \phi y \le \map \phi x + \epsilon \map d {x, x_0}$
Since $\phi$ is lower semicontinuous, we have:
:$\ds \map \phi {x_0} \le \liminf_{y \mathop \to x_0} \map \phi y$
We therefore have:
:$\map \phi {x_0} \le \map \phi x + \epsilon \map d {x, x_0}$ for each $x \in X$
and hence:
:$\map \phi x \ge \map \phi {x_0} - \epsilon \map d {x, x_0}$ for each $x \in X$.
{{qed}}
{{Namedfor|Ivar Ekeland|cat=Ekeland}}