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 #
contracting_with K f: a Lipschitz continuous self-map withK < 1;efixed_point: given a contracting mapfon a complete emetric space and a pointxsuch thatedist x (f x) ≠ ∞,efixed_point f hf x hxis the unique fixed point offinemetric.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
A map is said to be contracting_with K, if K < 1 and f is lipschitz_with K.
Equations
- contracting_with K f = (K < 1 ∧ lipschitz_with K f)
theorem
contracting_with.to_lipschitz_with
{α : Type u_1}
[emetric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f) :
lipschitz_with K f
theorem
contracting_with.one_sub_K_pos'
{α : Type u_1}
[emetric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f) :
theorem
contracting_with.one_sub_K_ne_zero
{α : Type u_1}
[emetric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f) :
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 ≠ ⊤) :
has_edist.edist x y ≤ (has_edist.edist x (f x) + has_edist.edist y (f y)) / (1 - ↑K)
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) :
has_edist.edist x y ≤ has_edist.edist x (f x) / (1 - ↑K)
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) :
x = y ∨ has_edist.edist x 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) :
contracting_with K (set.maps_to.restrict f 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}
[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
- contracting_with.efixed_point f hf x hx = classical.some _
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) ≠ ⊤) :
function.is_fixed_pt f (contracting_with.efixed_point f hf x hx)
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) ≠ ⊤) :
filter.tendsto (λ (n : ℕ), f^[n] x) filter.at_top (nhds (contracting_with.efixed_point f hf x hx))
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 : ℕ) :
has_edist.edist (f^[n] x) (contracting_with.efixed_point f hf x hx) ≤ has_edist.edist x (f x) * ↑K ^ n / (1 - ↑K)
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) ≠ ⊤) :
has_edist.edist x (contracting_with.efixed_point f hf x hx) ≤ has_edist.edist x (f x) / (1 - ↑K)
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) ≠ ⊤) :
has_edist.edist x (contracting_with.efixed_point f hf x hx) < ⊤
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 ≠ ⊤) :
contracting_with.efixed_point f hf x hx = contracting_with.efixed_point f hf y hy
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
- contracting_with.efixed_point' f hsc hsf hf x hxs hx = classical.some _
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) ≠ ⊤) :
function.is_fixed_pt f (contracting_with.efixed_point' f hsc hsf hf x hxs hx)
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) ≠ ⊤) :
has_edist.edist x (contracting_with.efixed_point' f hsc hsf hf x hxs hx) ≤ has_edist.edist x (f x) / (1 - ↑K)
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) ≠ ⊤) :
has_edist.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 : 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) :
theorem
contracting_with.dist_le_mul
{α : Type u_1}
[metric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f)
(x y : α) :
has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist 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) :
has_dist.dist x y ≤ has_dist.dist x (f x) / (1 - ↑K)
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
- contracting_with.fixed_point f hf = contracting_with.efixed_point f hf (classical.choice _inst_2) _
theorem
contracting_with.fixed_point_is_fixed_pt
{α : Type u_1}
[metric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f)
[nonempty α]
[complete_space α] :
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) :
x = contracting_with.fixed_point f hf
theorem
contracting_with.dist_fixed_point_le
{α : Type u_1}
[metric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f)
[nonempty α]
[complete_space α]
(x : α) :
has_dist.dist x (contracting_with.fixed_point f hf) ≤ has_dist.dist x (f x) / (1 - ↑K)
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 : ℕ) :
has_dist.dist (f^[n] x) (contracting_with.fixed_point f hf) ≤ 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 : contracting_with K f)
[nonempty α]
[complete_space α]
(x : α)
(n : ℕ) :
has_dist.dist (f^[n] x) (contracting_with.fixed_point f hf) ≤ has_dist.dist x (f x) * ↑K ^ n / (1 - ↑K)
theorem
contracting_with.tendsto_iterate_fixed_point
{α : Type u_1}
[metric_space α]
{K : nnreal}
{f : α → α}
(hf : contracting_with K f)
[nonempty α]
[complete_space α]
(x : α) :
filter.tendsto (λ (n : ℕ), f^[n] x) filter.at_top (nhds (contracting_with.fixed_point f hf))
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) :
has_dist.dist (contracting_with.fixed_point f hf) (contracting_with.fixed_point g hg) ≤ C / (1 - ↑K)
theorem
contracting_with.is_fixed_pt_fixed_point_iterate
{α : Type u_1}
[metric_space α]
{K : nnreal}
{f : α → α}
[nonempty α]
[complete_space α]
{n : ℕ}
(hf : contracting_with K 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.