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.
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.