Browder–Göhde–Kirk fixed-point theorem

TheoremBrowder–Göhde–Kirk fixed point theorem#✓fully proved

Let \(E\) be a uniformly convex real Banach space and let \(K \subseteq E\) be a nonempty, closed, bounded, convex set. If a map \(f : E \to E\) sends \(K\) into \(K\) and is nonexpansive on \(K\), that is, \(\|f(x) - f(y)\| \le \|x - y\|\) for all \(x, y \in K\), then \(f\) has a fixed point in \(K\): there is \(y \in K\) with \(f(y) = y\).

theorem browderGoehdeKirk_fixedPoint
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E] [CompleteSpace E]
    {K : Set E} (hK_nonempty : K.Nonempty) (hK_closed : IsClosed K)
    (hK_bounded : Bornology.IsBounded K) (hK_convex : Convex ℝ K)
    {f : E → E} (hf_maps : MapsTo f K K) (hf_lip : LipschitzOnWith 1 f K) :
    ∃ y ∈ K, f y = y

Sources

• F. Browder, Proc. Nat. Acad. Sci. USA 1965, D. Göhde, Math. Ann. 1965, and W. Kirk, Amer. Math. Monthly 1965-66, fixed-point theorem for nonexpansive mappings in uniformly convex Banach spaces; textbook Goebel and Kirk, 1990; Lean states complete uniformly convex real case with Bornology.IsBounded convex set.

DefinitionDiameter of a set#✓fully proved

The diameter of a set \(s\) in a real normed space is the supremum in \(\mathbb{R}\) of the distances \(\operatorname{dist}(x, y)\) over all \(x, y \in s\); by the convention for real suprema it is \(0\) when \(s\) is empty or these distances are unbounded.

noncomputable def metricDiameter (s : Set E) : ℝ :=
  sSup {r : ℝ | ∃ x ∈ s, ∃ y ∈ s, dist x y = r}

Used by 1

Used byDiametral point

DefinitionRadius of a point in a set#✓fully proved

The radius of a point \(x\) in a set \(s\) of a real normed space is the supremum in \(\mathbb{R}\) of the distances \(\operatorname{dist}(x, y)\) over all \(y \in s\); by the convention for real suprema it is \(0\) when \(s\) is empty or these distances are unbounded.

noncomputable def pointRadiusIn (x : E) (s : Set E) : ℝ :=
  sSup {r : ℝ | ∃ y ∈ s, dist x y = r}

Used by 1

Used byDiametral point

DefinitionDiametral point#✓fully proved

A point \(x\) of a real normed space is diametral in a set \(s\) if \(x \in s\) and the radius of \(x\) in \(s\) equals the diameter of \(s\).

def IsDiametralPoint (s : Set E) (x : E) : Prop :=
  x ∈ s ∧ pointRadiusIn x s = metricDiameter s

Uses 2 · Used by 1

Statement usesDiameter of a set · Radius of a point in a set

Used byNormal structure

DefinitionNormal structure#✓fully proved

A set \(K\) in a real normed space has normal structure if every convex subset \(H \subseteq K\) with at least two points contains a point that is not diametral in \(H\).

def HasNormalStructure (K : Set E) : Prop :=
  ∀ H : Set E,
    H ⊆ K →
      Convex ℝ H →
        H.Nontrivial →
          ∃ x ∈ H, ¬ IsDiametralPoint H x

Uses 1 · Used by 1

Statement usesDiametral point

Used byKirk's fixed-point theorem for sets with normal structure

DefinitionNonexpansive self-map#✓fully proved

A map \(T : K \to K\) from a subset \(K\) of a real normed space to itself is nonexpansive if \(\|T(x) - T(y)\| \le \|x - y\|\) for all \(x, y \in K\), that is, if \(T\) is \(1\)-Lipschitz for the distance inherited from the space.

def IsNonexpansiveSelfMap (K : Set E) (T : K → K) : Prop :=
  LipschitzWith 1 T

Used by 1

Used byKirk's fixed-point theorem for sets with normal structure

TheoremKirk's fixed-point theorem for sets with normal structure#●ready to prove

Let \(E\) be a reflexive real Banach space, meaning that the canonical embedding of \(E\) into its double dual is surjective, and let \(K \subseteq E\) be a nonempty, closed, bounded, convex set with normal structure. Then every nonexpansive self-map \(T : K \to K\) has a fixed point.

public theorem_wanted kirk_normal_structure [CompleteSpace E]
    (hE_reflexive : Function.Surjective (NormedSpace.inclusionInDoubleDual ℝ E))
    (K : Set E) (hK_nonempty : K.Nonempty) (hK_closed : IsClosed K)
    (hK_bounded : Bornology.IsBounded K) (hK_convex : Convex ℝ K)
    (hK_normal : HasNormalStructure K) (T : K → K)
    (hT : IsNonexpansiveSelfMap K T) :
    ∃ x : K, IsFixedPt T x

Sources

• W. A. Kirk, A fixed point theorem for mappings which do not increase distances, Amer. Math. Monthly 72 (1965). Listed as §228 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §228. Problem kirk_normal_structure of the lean-eval benchmark.

Uses 2

Statement usesNormal structure · Nonexpansive self-map

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.