English
Let s be a complete forward-invariant set; efixedPoint' is defined as the unique fixed point of the restriction of f to s ∩ ball_x(∞).
Русский
Пусть s полнота; efixedPoint' определяется как уникальная фиксированная точка ограниченного отображения f на s ∩ шар_x(∞).
LaTeX
$$$ \\text{efixedPoint'}\, f\, hsc\, hsf\, hf\, x\, hxs\, hx \\;\\text{ есть уникальная точка фиксации ограниченного отображения}.$$$
Lean4
/-- Banach fixed-point theorem, contraction mapping theorem, `EMetricSpace` version.
A contracting map on a complete metric space has a fixed point.
We include more conclusions in this theorem to avoid proving them again later.
The main API for this theorem are the functions `efixedPoint` and `fixedPoint`,
and lemmas about these functions. -/
theorem exists_fixedPoint (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ∞) :
∃ y,
IsFixedPt f y ∧
Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧ ∀ n : ℕ, edist (f^[n] x) y ≤ edist x (f x) * (K : ℝ≥0∞) ^ n / (1 - K) :=
have : CauchySeq fun n ↦ f^[n] x :=
cauchySeq_of_edist_le_geometric K (edist x (f x)) (ENNReal.coe_lt_one_iff.2 hf.1) hx
(hf.toLipschitzWith.edist_iterate_succ_le_geometric x)
let ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this
⟨y, isFixedPt_of_tendsto_iterate hy hf.2.continuous.continuousAt, hy,
edist_le_of_edist_le_geometric_of_tendsto K (edist x (f x)) (hf.toLipschitzWith.edist_iterate_succ_le_geometric x)
hy⟩
