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

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

Tags

contracting map, fixed point, Banach fixed point theorem

def ContractingWith {α : Type u_1} [EMetricSpace α] (K : NNReal) (f : α → α) : Prop

A map is said to be ContractingWith K, if K < 1 and f is LipschitzWith K.

Equations

• ContractingWith K f = (K < 1 ∧ LipschitzWith K f)

theorem ContractingWith.toLipschitzWith {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) : LipschitzWith K f

theorem ContractingWith.one_sub_K_pos' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) : 0 < 1 - ↑K

theorem ContractingWith.one_sub_K_ne_zero {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) : 1 - ↑K ≠ 0

theorem ContractingWith.one_sub_K_ne_top {K : NNReal} : 1 - ↑K ≠ ⊤

theorem ContractingWith.edist_inequality {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} {y : α} (h : edist x y ≠ ⊤) : edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)

theorem ContractingWith.edist_le_of_fixedPoint {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} {y : α} (h : edist x y ≠ ⊤) (hy : Function.IsFixedPt f y) : edist x y ≤ edist x (f x) / (1 - ↑K)

theorem ContractingWith.eq_or_edist_eq_top_of_fixedPoints {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} {y : α} (hx : Function.IsFixedPt f x) (hy : Function.IsFixedPt f y) : x = y ∨ edist x y = ⊤

theorem ContractingWith.restrict {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {s : Set α} (hs : Set.MapsTo f s s) : ContractingWith K (Set.MapsTo.restrict f s s hs)

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

theorem ContractingWith.exists_fixedPoint {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ⊤) : ∃ (y : α), Function.IsFixedPt f y ∧ Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Banach fixed-point theorem, contraction mapping theorem, EMetricSpace 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 efixedPoint and fixedPoint, and lemmas about these functions.

noncomputable def ContractingWith.efixedPoint {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} (f : α → α) (hf : ContractingWith K f) (x : α) (hx : 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 efixedPoint is the unique fixed point of f in EMetric.ball x ∞.

Equations

• ContractingWith.efixedPoint f hf x hx = Classical.choose ⋯

theorem ContractingWith.efixedPoint_isFixedPt {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ⊤) : Function.IsFixedPt f (ContractingWith.efixedPoint f hf x hx)

theorem ContractingWith.tendsto_iterate_efixedPoint {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ⊤) : Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds (ContractingWith.efixedPoint f hf x hx))

theorem ContractingWith.apriori_edist_iterate_efixedPoint_le {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ⊤) (n : ℕ) : edist (f^[n] x) (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

theorem ContractingWith.edist_efixedPoint_le {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ⊤) : edist x (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)

theorem ContractingWith.edist_efixedPoint_lt_top {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ⊤) : edist x (ContractingWith.efixedPoint f hf x hx) < ⊤

theorem ContractingWith.efixedPoint_eq_of_edist_lt_top {α : Type u_1} [EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ⊤) {y : α} (hy : edist y (f y) ≠ ⊤) (h : edist x y ≠ ⊤) : ContractingWith.efixedPoint f hf x hx = ContractingWith.efixedPoint f hf y hy

theorem ContractingWith.exists_fixedPoint' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) : ∃ y ∈ s, Function.IsFixedPt f y ∧ Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds 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.

noncomputable def ContractingWith.efixedPoint' {α : Type u_1} [EMetricSpace α] {K : NNReal} (f : α → α) {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) (x : α) (hxs : x ∈ s) (hx : 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 efixedPoint' is the unique fixed point of the restriction of f to s ∩ EMetric.ball x ∞.

Equations

• ContractingWith.efixedPoint' f hsc hsf hf x hxs hx = Classical.choose ⋯

theorem ContractingWith.efixedPoint_mem' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) : ContractingWith.efixedPoint' f hsc hsf hf x hxs hx ∈ s

theorem ContractingWith.efixedPoint_isFixedPt' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) : Function.IsFixedPt f (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx)

theorem ContractingWith.tendsto_iterate_efixedPoint' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) : Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx))

theorem ContractingWith.apriori_edist_iterate_efixedPoint_le' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) (n : ℕ) : edist (f^[n] x) (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

theorem ContractingWith.edist_efixedPoint_le' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) : edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)

theorem ContractingWith.edist_efixedPoint_lt_top' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) : edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) < ⊤

theorem ContractingWith.efixedPoint_eq_of_edist_lt_top' {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s) (hfs : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤) {t : Set α} (htc : IsComplete t) (htf : Set.MapsTo f t t) (hft : ContractingWith K (Set.MapsTo.restrict f t t htf)) {y : α} (hyt : y ∈ t) (hy : edist y (f y) ≠ ⊤) (hxy : edist x y ≠ ⊤) : ContractingWith.efixedPoint' f hsc hsf hfs x hxs hx = ContractingWith.efixedPoint' 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 efixedPoint' constructed by x is the same as the efixedPoint' 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 ContractingWith.one_sub_K_pos {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) : 0 < 1 - ↑K

theorem ContractingWith.dist_le_mul {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) (x : α) (y : α) : dist (f x) (f y) ≤ ↑K * dist x y

theorem ContractingWith.dist_inequality {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) (x : α) (y : α) : dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - ↑K)

theorem ContractingWith.dist_le_of_fixedPoint {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) (x : α) {y : α} (hy : Function.IsFixedPt f y) : dist x y ≤ dist x (f x) / (1 - ↑K)

theorem ContractingWith.fixedPoint_unique' {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) {x : α} {y : α} (hx : Function.IsFixedPt f x) (hy : Function.IsFixedPt f y) : x = y

theorem ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le' {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) (g : α → α) {x : α} {y : α} (hx : Function.IsFixedPt f x) (hy : Function.IsFixedPt g y) {C : ℝ} (hfg : ∀ (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).

noncomputable def ContractingWith.fixedPoint {α : Type u_1} [MetricSpace α] {K : NNReal} (f : α → α) (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] : α

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

Equations

• ContractingWith.fixedPoint f hf = ContractingWith.efixedPoint f hf (Classical.choice inst✝) ⋯

theorem ContractingWith.fixedPoint_isFixedPt {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] : Function.IsFixedPt f (ContractingWith.fixedPoint f hf)

The point provided by ContractingWith.fixedPoint is actually a fixed point.

theorem ContractingWith.fixedPoint_unique {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] {x : α} (hx : Function.IsFixedPt f x) : x = ContractingWith.fixedPoint f hf

theorem ContractingWith.dist_fixedPoint_le {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] (x : α) : dist x (ContractingWith.fixedPoint f hf) ≤ dist x (f x) / (1 - ↑K)

theorem ContractingWith.aposteriori_dist_iterate_fixedPoint_le {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] (x : α) (n : ℕ) : dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)

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

theorem ContractingWith.apriori_dist_iterate_fixedPoint_le {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] (x : α) (n : ℕ) : dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist x (f x) * ↑K ^ n / (1 - ↑K)

theorem ContractingWith.tendsto_iterate_fixedPoint {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] (x : α) : Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds (ContractingWith.fixedPoint f hf))

theorem ContractingWith.fixedPoint_lipschitz_in_map {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] {g : α → α} (hg : ContractingWith K g) {C : ℝ} (hfg : ∀ (z : α), dist (f z) (g z) ≤ C) : dist (ContractingWith.fixedPoint f hf) (ContractingWith.fixedPoint g hg) ≤ C / (1 - ↑K)

theorem ContractingWith.isFixedPt_fixedPoint_iterate {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} [Nonempty α] [CompleteSpace α] {n : ℕ} (hf : ContractingWith K f^[n]) : Function.IsFixedPt f (ContractingWith.fixedPoint f^[n] hf)

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