mathlib3 documentation

topology.metric_space.contracting

Contracting maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Tags #

contracting map, fixed point, Banach fixed point theorem

def contracting_with {α : Type u_1} [emetric_space α] (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} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) :
theorem contracting_with.one_sub_K_pos' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) :
0 < 1 - K
theorem contracting_with.one_sub_K_ne_zero {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) :
1 - K 0
theorem contracting_with.edist_inequality {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x y : α} (h : has_edist.edist x y ) :
theorem contracting_with.edist_le_of_fixed_point {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x y : α} (h : has_edist.edist x y ) (hy : function.is_fixed_pt f y) :
theorem contracting_with.eq_or_edist_eq_top_of_fixed_points {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x y : α} (hx : function.is_fixed_pt f x) (hy : function.is_fixed_pt f y) :
theorem contracting_with.restrict {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {s : set α} (hs : set.maps_to f s s) :

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} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) (x : α) (hx : has_edist.edist x (f x) ) :
(y : α), function.is_fixed_pt f y filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds y) (n : ), has_edist.edist (f^[n] x) y has_edist.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.

noncomputable def contracting_with.efixed_point {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} (f : α α) (hf : contracting_with K f) (x : α) (hx : has_edist.edist 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
theorem contracting_with.efixed_point_is_fixed_pt {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x : α} (hx : has_edist.edist x (f x) ) :
theorem contracting_with.tendsto_iterate_efixed_point {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x : α} (hx : has_edist.edist x (f x) ) :
theorem contracting_with.apriori_edist_iterate_efixed_point_le {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x : α} (hx : has_edist.edist x (f x) ) (n : ) :
theorem contracting_with.edist_efixed_point_le {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x : α} (hx : has_edist.edist x (f x) ) :
theorem contracting_with.edist_efixed_point_lt_top {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x : α} (hx : has_edist.edist x (f x) ) :
theorem contracting_with.efixed_point_eq_of_edist_lt_top {α : Type u_1} [emetric_space α] [cs : complete_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x : α} (hx : has_edist.edist x (f x) ) {y : α} (hy : has_edist.edist y (f y) ) (h : has_edist.edist x y ) :
theorem contracting_with.exists_fixed_point' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) :
(y : α) (H : y s), function.is_fixed_pt f y filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds y) (n : ), has_edist.edist (f^[n] x) y has_edist.edist x (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} [emetric_space α] {K : nnreal} (f : α α) {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) (x : α) (hxs : x s) (hx : has_edist.edist x (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
theorem contracting_with.efixed_point_mem' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) :
contracting_with.efixed_point' f hsc hsf hf x hxs hx s
theorem contracting_with.efixed_point_is_fixed_pt' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) :
theorem contracting_with.tendsto_iterate_efixed_point' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (nhds (contracting_with.efixed_point' f hsc hsf hf x hxs hx))
theorem contracting_with.apriori_edist_iterate_efixed_point_le' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) (n : ) :
has_edist.edist (f^[n] x) (contracting_with.efixed_point' f hsc hsf hf x hxs hx) has_edist.edist x (f x) * K ^ n / (1 - K)
theorem contracting_with.edist_efixed_point_le' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) :
theorem contracting_with.edist_efixed_point_lt_top' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hf : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) :
theorem contracting_with.efixed_point_eq_of_edist_lt_top' {α : Type u_1} [emetric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {s : set α} (hsc : is_complete s) (hsf : set.maps_to f s s) (hfs : contracting_with K (set.maps_to.restrict f s s hsf)) {x : α} (hxs : x s) (hx : has_edist.edist x (f x) ) {t : set α} (htc : is_complete t) (htf : set.maps_to f t t) (hft : contracting_with K (set.maps_to.restrict f t t htf)) {y : α} (hyt : y t) (hy : has_edist.edist y (f y) ) (hxy : has_edist.edist x y ) :
contracting_with.efixed_point' f hsc hsf hfs x hxs hx = contracting_with.efixed_point' f htc 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 : contracting_with K f) :
0 < 1 - K
theorem contracting_with.dist_le_mul {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) (x y : α) :
theorem contracting_with.dist_inequality {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) (x y : α) :
has_dist.dist x y (has_dist.dist x (f x) + has_dist.dist y (f y)) / (1 - K)
theorem contracting_with.dist_le_of_fixed_point {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) (x : α) {y : α} (hy : function.is_fixed_pt f y) :
theorem contracting_with.fixed_point_unique' {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) {x y : α} (hx : function.is_fixed_pt f x) (hy : function.is_fixed_pt f y) :
x = y
theorem contracting_with.dist_fixed_point_fixed_point_of_dist_le' {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) (g : α α) {x y : α} (hx : function.is_fixed_pt f x) (hy : function.is_fixed_pt g y) {C : } (hfg : (z : α), has_dist.dist (f z) (g z) C) :
has_dist.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).

noncomputable def contracting_with.fixed_point {α : Type u_1} [metric_space α] {K : nnreal} (f : α α) (hf : contracting_with K f) [nonempty α] [complete_space α] :
α

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

Equations

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 : contracting_with K f) [nonempty α] [complete_space α] {x : α} (hx : function.is_fixed_pt f x) :
theorem contracting_with.dist_fixed_point_le {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) [nonempty α] [complete_space α] (x : α) :
theorem contracting_with.aposteriori_dist_iterate_fixed_point_le {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) [nonempty α] [complete_space α] (x : α) (n : ) :

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 : contracting_with K f) [nonempty α] [complete_space α] (x : α) (n : ) :
theorem contracting_with.fixed_point_lipschitz_in_map {α : Type u_1} [metric_space α] {K : nnreal} {f : α α} (hf : contracting_with K f) [nonempty α] [complete_space α] {g : α α} (hg : contracting_with K g) {C : } (hfg : (z : α), has_dist.dist (f z) (g z) C) :

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