English
There exists a fixed point for the restricted contracting map in the forward-complete setting.
Русский
Существует фиксированная точка ограниченного отображения в контексте полной области.
LaTeX
$$$ \exists y \in s, \text{IsFixedPt}(f,y) \land \text{Tendsto}(f^{[n]} x) \to y \land \cdots $$$
Lean4
/-- Banach fixed-point theorem for maps contracting on a complete subset. -/
theorem exists_fixedPoint' {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
(hf : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
∃ y ∈ s,
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) :=
by
haveI := hsc.completeSpace_coe
rcases hf.exists_fixedPoint ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩
refine ⟨y, y.2, Subtype.ext_iff.1 hfy, ?_, fun n ↦ ?_⟩
· convert (continuous_subtype_val.tendsto _).comp h_tendsto
simp only [(· ∘ ·), MapsTo.iterate_restrict, MapsTo.val_restrict_apply]
· convert hle n
rw [MapsTo.iterate_restrict]
rfl
