# mathlibdocumentation

topology.metric_space.contracting

# Contracting maps

A Lipschitz continuous self-map with Lipschitz constant K < 1 is called a contracting map. In this file we prove the Banach fixed point theorem, some explicit estimates on the rate of convergence, and some properties of the map sending a contracting map to its fixed point.

## Main definitions

• contracting_with K f : a Lipschitz continuous self-map with K < 1;
• efixed_point : given a contracting map f on a complete emetric space and a point x such that edist x (f x) < ∞, efixed_point f hf x hx is the unique fixed point of f in emetric.ball x ∞;
• fixed_point : the unique fixed point of a contracting map on a complete nonempty metric space.

## Tags

contracting map, fixed point, Banach fixed point theorem

def contracting_with {α : Type u_1}  :
ℝ≥0(α → α) → Prop

A map is said to be contracting_with K, if K < 1 and f is lipschitz_with K.

Equations
theorem contracting_with.to_lipschitz_with {α : Type u_1} {K : ℝ≥0} {f : α → α} :

theorem contracting_with.one_sub_K_pos' {α : Type u_1} {K : ℝ≥0} {f : α → α} :
0 < 1 - K

theorem contracting_with.one_sub_K_ne_zero {α : Type u_1} {K : ℝ≥0} {f : α → α} :
1 - K 0

theorem contracting_with.edist_inequality {α : Type u_1} {K : ℝ≥0} {f : α → α} (hf : f) {x y : α} :
y < y (edist x (f x) + (f y)) / (1 - K)

theorem contracting_with.edist_le_of_fixed_point {α : Type u_1} {K : ℝ≥0} {f : α → α} (hf : f) {x y : α} :
y < y (f x) / (1 - K)

theorem contracting_with.eq_or_edist_eq_top_of_fixed_points {α : Type u_1} {K : ℝ≥0} {f : α → α} (hf : f) {x y : α} :
x = y y =

theorem contracting_with.restrict {α : Type u_1} {K : ℝ≥0} {f : α → α} (hf : f) {s : set α} (hs : s s) :
s hs)

If a map f is contracting_with K, and s is a forward-invariant set, then restriction of f to s is contracting_with K as well.

theorem contracting_with.exists_fixed_point {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) (x : α) :
(f x) < (∃ (y : α), filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 y) ∀ (n : ), edist (f^[n] x) y (edist x (f x)) * K ^ n / (1 - K))

Banach fixed-point theorem, contraction mapping theorem, emetric_space 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 efixed_point and fixed_point, and lemmas about these functions.

def contracting_with.efixed_point {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} (f : α → α) (hf : f) (x : α) :
(f x) < → α

Let x be a point of a complete emetric space. Suppose that f is a contracting map, and edist x (f x) < ∞. Then efixed_point is the unique fixed point of f in emetric.ball x ∞.

Equations
• hx =
theorem contracting_with.efixed_point_is_fixed_pt {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x : α} (hx : (f x) < ) :
hx)

theorem contracting_with.tendsto_iterate_efixed_point {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x : α} (hx : (f x) < ) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 hx))

theorem contracting_with.apriori_edist_iterate_efixed_point_le {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x : α} (hx : (f x) < ) (n : ) :
edist (f^[n] x) hx) (edist x (f x)) * K ^ n / (1 - K)

theorem contracting_with.edist_efixed_point_le {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x : α} (hx : (f x) < ) :
hx) (f x) / (1 - K)

theorem contracting_with.edist_efixed_point_lt_top {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x : α} (hx : (f x) < ) :
hx) <

theorem contracting_with.efixed_point_eq_of_edist_lt_top {α : Type u_1} [cs : complete_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x : α} (hx : (f x) < ) {y : α} (hy : (f y) < ) :
y < hx = hy

theorem contracting_with.exists_fixed_point' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} :
x s (f x) < (∃ (y : α) (H : y s), filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 y) ∀ (n : ), edist (f^[n] x) y (edist x (f x)) * K ^ n / (1 - K))

Banach fixed-point theorem for maps contracting on a complete subset.

def contracting_with.efixed_point' {α : Type u_1} {K : ℝ≥0} (f : α → α) {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) (x : α) :
x s (f x) < → α

Let s be a complete forward-invariant set of a self-map f. If f contracts on s and x ∈ s satisfies edist x (f x) < ⊤, then efixed_point' is the unique fixed point of the restriction of f to s ∩ emetric.ball x ⊤.

Equations
• hsf hf x hxs hx =
theorem contracting_with.efixed_point_mem' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) :
hsf hf x hxs hx s

theorem contracting_with.efixed_point_is_fixed_pt' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) :
hsf hf x hxs hx)

theorem contracting_with.tendsto_iterate_efixed_point' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 hsf hf x hxs hx))

theorem contracting_with.apriori_edist_iterate_efixed_point_le' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) (n : ) :
edist (f^[n] x) hsf hf x hxs hx) (edist x (f x)) * K ^ n / (1 - K)

theorem contracting_with.edist_efixed_point_le' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) :
hsf hf x hxs hx) (f x) / (1 - K)

theorem contracting_with.edist_efixed_point_lt_top' {α : Type u_1} {K : ℝ≥0} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) :
hsf hf x hxs hx) <

theorem contracting_with.efixed_point_eq_of_edist_lt_top' {α : Type u_1} {K : ℝ≥0} {f : α → α} (hf : f) {s : set α} (hsc : is_complete s) (hsf : s s) (hfs : s hsf)) {x : α} (hxs : x s) (hx : (f x) < ) {t : set α} (htc : is_complete t) (htf : t t) (hft : t htf)) {y : α} (hyt : y t) (hy : (f y) < ) :
y < hsf hfs x hxs hx = htf hft y hyt hy

If a globally contracting map f has two complete forward-invariant sets s, t, and x ∈ s is at a finite distance from y ∈ t, then the efixed_point' constructed by x is the same as the efixed_point' constructed by y.

This lemma takes additional arguments stating that f contracts on s and t because this way it can be used to prove the desired equality with non-trivial proofs of these facts.

theorem contracting_with.one_sub_K_pos {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} :
0 < 1 - K

theorem contracting_with.dist_le_mul {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) (x y : α) :
dist (f x) (f y) (K) * dist x y

theorem contracting_with.dist_inequality {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) (x y : α) :
dist x y (dist x (f x) + dist y (f y)) / (1 - K)

theorem contracting_with.dist_le_of_fixed_point {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) (x : α) {y : α} :
dist x y dist x (f x) / (1 - K)

theorem contracting_with.fixed_point_unique' {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) {x y : α} :
x = y

theorem contracting_with.dist_fixed_point_fixed_point_of_dist_le' {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) (g : α → α) {x y : α} (hx : x) (hy : y) {C : } :
(∀ (z : α), dist (f z) (g z) C)dist x y C / (1 - K)

Let f be a contracting map with constant K; let g be another map uniformly C-close to f. If x and y are their fixed points, then dist x y ≤ C / (1 - K).

def contracting_with.fixed_point {α : Type u_1} [metric_space α] {K : ℝ≥0} (f : α → α) (hf : f) [nonempty α]  :
α

The unique fixed point of a contracting map in a nonempty complete metric space.

Equations
theorem contracting_with.fixed_point_is_fixed_pt {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α]  :

The point provided by contracting_with.fixed_point is actually a fixed point.

theorem contracting_with.fixed_point_unique {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α] {x : α} :

theorem contracting_with.dist_fixed_point_le {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α] (x : α) :
dist x dist x (f x) / (1 - K)

theorem contracting_with.aposteriori_dist_iterate_fixed_point_le {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α] (x : α) (n : ) :
dist (f^[n] x) dist (f^[n] x) (f^[n + 1] x) / (1 - K)

Aposteriori estimates on the convergence of iterates to the fixed point.

theorem contracting_with.apriori_dist_iterate_fixed_point_le {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α] (x : α) (n : ) :
dist (f^[n] x) (dist x (f x)) * K ^ n / (1 - K)

theorem contracting_with.tendsto_iterate_fixed_point {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α] (x : α) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 hf))

theorem contracting_with.fixed_point_lipschitz_in_map {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : f) [nonempty α] {g : α → α} (hg : g) {C : } :
(∀ (z : α), dist (f z) (g z) C) C / (1 - K)