mathlib documentation

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

Tags

contracting map, fixed point, Banach fixed point theorem

def contracting_with {α : Type u_1} [emetric_space α] :
ℝ≥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} [emetric_space α] {K : ℝ≥0} {f : α → α} :

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

theorem contracting_with.one_sub_K_ne_zero {α : Type u_1} [emetric_space α] {K : ℝ≥0} {f : α → α} :
contracting_with K f1 - K 0

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

theorem contracting_with.edist_le_of_fixed_point {α : Type u_1} [emetric_space α] {K : ℝ≥0} {f : α → α} (hf : contracting_with K f) {x y : α} :
edist x y < function.is_fixed_pt f yedist x y edist x (f x) / (1 - K)

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

theorem contracting_with.restrict {α : Type u_1} [emetric_space α] {K : ℝ≥0} {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 : ℝ≥0} {f : α → α} (hf : contracting_with K f) (x : α) :
edist x (f x) < (∃ (y : α), function.is_fixed_pt f 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} [emetric_space α] [cs : complete_space α] {K : ℝ≥0} (f : α → α) (hf : contracting_with K f) (x : α) :
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 : ℝ≥0} {f : α → α} (hf : contracting_with K f) {x : α} (hx : edist x (f x) < ) :

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

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

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

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

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

theorem contracting_with.exists_fixed_point' {α : Type u_1} [emetric_space α] {K : ℝ≥0} {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 : α} :
x sedist x (f x) < (∃ (y : α) (H : y s), function.is_fixed_pt f 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 for maps contracting on a complete subset.

def contracting_with.efixed_point' {α : Type u_1} [emetric_space α] {K : ℝ≥0} (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 : α) :
x sedist 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 : ℝ≥0} {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 : 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 : ℝ≥0} {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 : edist x (f x) < ) :

theorem contracting_with.tendsto_iterate_efixed_point' {α : Type u_1} [emetric_space α] {K : ℝ≥0} {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 : edist x (f x) < ) :
filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 (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 : ℝ≥0} {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 : edist x (f x) < ) (n : ) :
edist (f^[n] x) (contracting_with.efixed_point' f hsc hsf hf x hxs hx) (edist x (f x)) * K ^ n / (1 - K)

theorem contracting_with.edist_efixed_point_le' {α : Type u_1} [emetric_space α] {K : ℝ≥0} {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 : edist x (f x) < ) :
edist x (contracting_with.efixed_point' f hsc hsf hf x hxs hx) edist x (f x) / (1 - K)

theorem contracting_with.edist_efixed_point_lt_top' {α : Type u_1} [emetric_space α] {K : ℝ≥0} {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 : edist x (f x) < ) :
edist x (contracting_with.efixed_point' f hsc hsf hf x hxs hx) <

theorem contracting_with.efixed_point_eq_of_edist_lt_top' {α : Type u_1} [emetric_space α] {K : ℝ≥0} {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 : 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 : edist y (f y) < ) :
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 : ℝ≥0} {f : α → α} :
contracting_with K f0 < 1 - K

theorem contracting_with.dist_le_mul {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : contracting_with K 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 : contracting_with K 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 : contracting_with K f) (x : α) {y : α} :
function.is_fixed_pt f ydist x y dist x (f x) / (1 - K)

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

theorem contracting_with.dist_fixed_point_fixed_point_of_dist_le' {α : Type u_1} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : contracting_with K f) (g : α → α) {x y : α} (hx : function.is_fixed_pt f x) (hy : function.is_fixed_pt g 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 : 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 : ℝ≥0} {f : α → α} (hf : contracting_with K f) [nonempty α] [complete_space α] {x : α} :

theorem contracting_with.dist_fixed_point_le {α : Type u_1} [metric_space α] {K : ℝ≥0} {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 : ℝ≥0} {f : α → α} (hf : contracting_with K f) [nonempty α] [complete_space α] (x : α) (n : ) :
dist (f^[n] x) (contracting_with.fixed_point f hf) 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 : contracting_with K f) [nonempty α] [complete_space α] (x : α) (n : ) :
dist (f^[n] x) (contracting_with.fixed_point f hf) (dist x (f x)) * K ^ n / (1 - K)

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

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