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} (K : nnreal) (f : α → α) :
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 : nnreal} {f : α → α} (hf : f) :
theorem contracting_with.one_sub_K_pos' {α : Type u_1} {K : nnreal} {f : α → α} (hf : f) :
0 < 1 - K
theorem contracting_with.one_sub_K_ne_zero {α : Type u_1} {K : nnreal} {f : α → α} (hf : f) :
1 - K 0
theorem contracting_with.edist_inequality {α : Type u_1} {K : nnreal} {f : α → α} (hf : f) {x y : α} (h : ) :
(f x) + (f y)) / (1 - K)
theorem contracting_with.edist_le_of_fixed_point {α : Type u_1} {K : nnreal} {f : α → α} (hf : f) {x y : α} (h : ) (hy : y) :
(f x) / (1 - K)
theorem contracting_with.eq_or_edist_eq_top_of_fixed_points {α : Type u_1} {K : nnreal} {f : α → α} (hf : f) {x y : α} (hx : x) (hy : y) :
x = y
theorem contracting_with.restrict {α : Type u_1} {K : nnreal} {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 : nnreal} {f : α → α} (hf : f) (x : α) (hx : (f x) ) :
∃ (y : α), filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds y) ∀ (n : ), has_edist.edist (f^[n] x) y (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.

noncomputable def contracting_with.efixed_point {α : Type u_1} [cs : complete_space α] {K : nnreal} (f : α → α) (hf : f) (x : α) (hx : (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 : nnreal} {f : α → α} (hf : f) {x : α} (hx : (f x) ) :
hx)
theorem contracting_with.tendsto_iterate_efixed_point {α : Type u_1} [cs : complete_space α] {K : nnreal} {f : α → α} (hf : f) {x : α} (hx : (f x) ) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds hx))
theorem contracting_with.apriori_edist_iterate_efixed_point_le {α : Type u_1} [cs : complete_space α] {K : nnreal} {f : α → α} (hf : f) {x : α} (hx : (f x) ) (n : ) :
has_edist.edist (f^[n] x) hx) (f x) * K ^ n / (1 - K)
theorem contracting_with.edist_efixed_point_le {α : Type u_1} [cs : complete_space α] {K : nnreal} {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 : nnreal} {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 : nnreal} {f : α → α} (hf : f) {x : α} (hx : (f x) ) {y : α} (hy : (f y) ) (h : ) :
hx = hy
theorem contracting_with.exists_fixed_point' {α : Type u_1} {K : nnreal} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) ) :
∃ (y : α) (H : y s), filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds y) ∀ (n : ), has_edist.edist (f^[n] x) y (f x) * K ^ n / (1 - K)

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

noncomputable def contracting_with.efixed_point' {α : Type u_1} {K : nnreal} (f : α → α) {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) (x : α) (hxs : x s) (hx : (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 : nnreal} {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 : nnreal} {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 : nnreal} {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 (nhds hsf hf x hxs hx))
theorem contracting_with.apriori_edist_iterate_efixed_point_le' {α : Type u_1} {K : nnreal} {f : α → α} {s : set α} (hsc : is_complete s) (hsf : s s) (hf : s hsf)) {x : α} (hxs : x s) (hx : (f x) ) (n : ) :
has_edist.edist (f^[n] x) hsf hf x hxs hx) (f x) * K ^ n / (1 - K)
theorem contracting_with.edist_efixed_point_le' {α : Type u_1} {K : nnreal} {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 : nnreal} {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 : nnreal} {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) ) (hxy : ) :
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 : nnreal} {f : α → α} (hf : f) :
0 < 1 - K
theorem contracting_with.dist_le_mul {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) (x y : α) :
has_dist.dist (f x) (f y) K *
theorem contracting_with.dist_inequality {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) (x y : α) :
(f x) + (f y)) / (1 - K)
theorem contracting_with.dist_le_of_fixed_point {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) (x : α) {y : α} (hy : y) :
(f x) / (1 - K)
theorem contracting_with.fixed_point_unique' {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) {x y : α} (hx : x) (hy : y) :
x = y
theorem contracting_with.dist_fixed_point_fixed_point_of_dist_le' {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) (g : α → α) {x y : α} (hx : x) (hy : y) {C : } (hfg : ∀ (z : α), has_dist.dist (f z) (g z) C) :
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).

noncomputable def contracting_with.fixed_point {α : Type u_1} [metric_space α] {K : nnreal} (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 : nnreal} {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 : nnreal} {f : α → α} (hf : f) [nonempty α] {x : α} (hx : x) :
theorem contracting_with.dist_fixed_point_le {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) [nonempty α] (x : α) :
(f x) / (1 - K)
theorem contracting_with.aposteriori_dist_iterate_fixed_point_le {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) [nonempty α] (x : α) (n : ) :
has_dist.dist (f^[n] x) has_dist.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 : nnreal} {f : α → α} (hf : f) [nonempty α] (x : α) (n : ) :
has_dist.dist (f^[n] x) (f x) * K ^ n / (1 - K)
theorem contracting_with.tendsto_iterate_fixed_point {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) [nonempty α] (x : α) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds hf))
theorem contracting_with.fixed_point_lipschitz_in_map {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} (hf : f) [nonempty α] {g : α → α} (hg : g) {C : } (hfg : ∀ (z : α), has_dist.dist (f z) (g z) C) :
C / (1 - K)
theorem contracting_with.is_fixed_pt_fixed_point_iterate {α : Type u_1} [metric_space α] {K : nnreal} {f : α → α} [nonempty α] {n : } (hf : f^[n]) :

If a map f has a contracting iterate f^[n], then the fixed point of f^[n] is also a fixed point of f.