Ekeland variational principle
TheoremEkeland variational principle without a nonemptiness assumption#✓fully proved
Let \((X, d)\) be a complete metric space, let \(f : X \to \mathbb{R}\) be lower semicontinuous and bounded below, and let \(\varepsilon > 0\). If \(x_0 \in X\) satisfies \(f(x_0) \le f(x) + \varepsilon\) for every \(x \in X\), then there is \(x_\varepsilon \in X\) with \(f(x_\varepsilon) \le f(x_0)\), \(d(x_\varepsilon, x_0) \le 1\), and \(f(x_\varepsilon) < f(y) + \varepsilon\, d(x_\varepsilon, y)\) for every \(y \ne x_\varepsilon\).
The space \(X\) is not separately assumed nonempty, since the point \(x_0\) already lies in it.
theorem ekeland_variational_principle_general
{X : Type*} [MetricSpace X] [CompleteSpace X]
{f : X → ℝ} (hf_lsc : LowerSemicontinuous f)
(hf_bdd : BddBelow (range f))
{ε : ℝ} (hε : 0 < ε)
{x₀ : X} (hx₀ : ∀ x, f x₀ ≤ f x + ε) :
∃ xε : X, f xε ≤ f x₀ ∧ dist xε x₀ ≤ 1 ∧
∀ y, y ≠ xε → f xε < f y + ε * dist xε y
Used by 1
TheoremEkeland variational principle#✓fully proved
Let \((X, d)\) be a nonempty complete metric space, let \(f : X \to \mathbb{R}\) be lower semicontinuous and bounded below, and let \(\varepsilon > 0\). If \(x_0 \in X\) satisfies \(f(x_0) \le f(x) + \varepsilon\) for every \(x \in X\), then there is \(x_\varepsilon \in X\) with \(f(x_\varepsilon) \le f(x_0)\), \(d(x_\varepsilon, x_0) \le 1\), and \(f(x_\varepsilon) < f(y) + \varepsilon\, d(x_\varepsilon, y)\) for every \(y \ne x_\varepsilon\).
theorem ekeland_variational_principle
{X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X]
{f : X → ℝ} (hf_lsc : LowerSemicontinuous f)
(hf_bdd : BddBelow (range f))
{ε : ℝ} (hε : 0 < ε)
{x₀ : X} (hx₀ : ∀ x, f x₀ ≤ f x + ε) :
∃ xε : X, f xε ≤ f x₀ ∧ dist xε x₀ ≤ 1 ∧
∀ y, y ≠ xε → f xε < f y + ε * dist xε y
Sources
- I. Ekeland, J. Math. Anal. Appl. 47 (1974), 324-353, DOI 10.1016/0022-247X(74)90025-0. It follows from
ekeland_variational_principle_general; the instance[Nonempty X]is unused and keeps the source's shape.
Uses 1
TheoremCaristi fixed-point theorem#✓fully proved
Let \((X, d)\) be a nonempty complete metric space and let \(\varphi : X \to \mathbb{R}\) be lower semicontinuous and bounded below. If a map \(T : X \to X\) satisfies \(d(x, T x) \le \varphi(x) - \varphi(T x)\) for every \(x \in X\), then \(T\) has a fixed point: there is \(x \in X\) with \(T x = x\).
theorem caristi_fixedPoint
{X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X]
{φ : X → ℝ} (hφ_lsc : LowerSemicontinuous φ)
(hφ_bdd : BddBelow (range φ))
{T : X → X} (hT : ∀ x, dist x (T x) ≤ φ x - φ (T x)) :
∃ x, T x = x
Sources
- J. Caristi, Trans. Amer. Math. Soc. 215 (1976), 241-251, DOI 10.1090/S0002-9947-1976-0394329-4.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.