Fixed-point theory

Fixed points of nonexpansive, Lipschitz and affine maps: the Browder–Göhde–Kirk theorem and Kirk's normal structure, Markov–Kakutani, Browder's demiclosedness principle, maps with contracting iterates.

• Browder's demiclosedness principle
• Browder–Göhde–Kirk fixed-point theorem

TheoremFixed points of maps whose iterates have null Lipschitz constants#●ready to prove

Let \(X\) be a nonempty complete metric space, let \(f : X \to X\), and write \(f^n\) for the \(n\)-th iterate of \(f\). Let \((q_n)_{n \in \mathbb{N}}\) be a sequence of nonnegative real numbers with \(q_n \to 0\) such that \(d(f^n(x), f^n(y)) \le q_n \, d(x, y)\) for every \(n \ge 1\) and all \(x, y \in X\). Then \(f\) has a fixed point: there is \(x \in X\) with \(f(x) = x\).

public theorem_wanted exists_fixedPoint_of_iterate_lipschitz_tendsto_zero
    (X : Type*) [MetricSpace X] [CompleteSpace X] [Nonempty X] (f : X → X) (q : ℕ → ℝ)
    (hq_nonneg : ∀ n : ℕ, 0 ≤ q n)
    (hLip : ∀ n : ℕ+, ∀ x y : X, dist ((f^[n]) x) ((f^[n]) y) ≤ q n * dist x y)
    (hq_null : Tendsto q atTop (𝓝 (0 : ℝ))) :
    ∃ x : X, f x = x

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Operator theory; Nonlinear operators and their properties), problem ma_proofbench_l1_74.

TheoremMarkov–Kakutani fixed-point theorem#✓fully proved

Let \(K\) be a nonempty compact convex subset of a real normed space \(E\), and let \((F_i)_{i \in I}\) be a family of continuous affine maps \(E \to E\) such that each \(F_i\) maps \(K\) into \(K\) and \(F_i(F_j(x)) = F_j(F_i(x))\) for all \(i, j \in I\) and all \(x \in E\). Then there is \(x \in K\) with \(F_i(x) = x\) for every \(i \in I\).

Commutation is required on all of \(E\), not only on \(K\).

theorem markovKakutani_commonFixedPoint
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {K : Set E} (hK_nonempty : K.Nonempty) (hK_compact : IsCompact K)
    (hK_convex : Convex ℝ K)
    {ι : Type*} (F : ι → E →ᴬ[ℝ] E)
    (hF_maps : ∀ i, MapsTo (F i) K K)
    (hF_comm : ∀ i j : ι, ∀ x : E, F i (F j x) = F j (F i x)) :
    ∃ x ∈ K, ∀ i, F i x = x

Sources

• A. Markov, C. R. Acad. Sci. URSS 1936 and S. Kakutani, Proc. Imp. Acad. Tokyo 14 (1938) 242-245, Markov-Kakutani fixed-point theorem; Lean states real normed nonempty compact convex case with globally commuting E →ᴬ[ℝ] E family.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.