ContractingWith.efixedPoint_isFixedPt
theorem ContractingWith.efixedPoint_isFixedPt :
∀ {α : Type u_1} [inst : 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)
The theorem `ContractingWith.efixedPoint_isFixedPt` states that for any type `α` which is a complete metric space, for any non-negative real number `K`, and any function `f` from `α` to `α`, if `f` is a contracting map with contraction constant `K`, and for any point `x` in `α` where the extended distance between `x` and `f(x)` is not infinite, the function `efixedPoint` applied to `f`, the proof that `f` is contracting, `x`, and the proof that the distance between `x` and `f(x)` is not infinite, is a fixed point of `f`. In other words, the unique fixed point of a contracting function in the complete metric space, which lies within any distance of a given point, is indeed a fixed point of the function.
More concisely: If `α` is a complete metric space, `f: α → α` is a contracting map with constant `K`, and `x ∈ α` has finite distance to `f(x)`, then `efixedPoint f x` is a fixed point of `f`.
|
ContractingWith.restrict
theorem ContractingWith.restrict :
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
ContractingWith K f → ∀ {s : Set α} (hs : Set.MapsTo f s s), ContractingWith K (Set.MapsTo.restrict f s s hs)
The theorem `ContractingWith.restrict` states that given a function `f` and a set `s`, if `f` is a contracting map with constant `K` (meaning that `K` is less than 1 and `f` is `K`-Lipschitz) and `s` is a forward-invariant set under `f` (i.e., all images of elements in `s` under `f` remain within `s`), then the restriction of `f` to `s` remains a contracting map with the same constant `K`. This is to say, the contractive property is retained when the function is restricted to operate on a forward-invariant set.
More concisely: If `f` is a `K`-Lipschitz, contracting map on a forward-invariant set `s`, then the restriction `f|s` is also a `K`-Lipschitz, contracting map.
|
ContractingWith.aposteriori_dist_iterate_fixedPoint_le
theorem ContractingWith.aposteriori_dist_iterate_fixedPoint_le :
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
[inst_2 : CompleteSpace α] (x : α) (n : ℕ),
dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)
This theorem states that for any metric space (α, dist) that is nonempty and complete, any nonnegative real number K less than 1, and any function `f` from `α` to `α` that is a `K`-contracting map, the distance between the `n`-th iterate of `f` at `x` and the unique fixed point of `f` is less than or equal to the distance between the `n`-th iterate of `f` at `x` and the `(n + 1)`-th iterate of `f` at `x` divided by `(1 - K)`. The `n`-th iterate of `f` at `x` is obtained by applying `f` `n` times to `x`, and the unique fixed point of `f` is a point in the metric space that is mapped to itself by `f`. This theorem provides an a posteriori estimate of how quickly the iterates of `f` converge to its fixed point in terms of the contraction rate `K` and the distance between successive iterates of `f`.
More concisely: For any complete, nonempty metric space (α, dist), any nonnegative real number K < 1, and any K-contracting map f from α to α, the distance between the n-th iterate of f at x and the unique fixed point of f is less than or equal to the distance between the n-th and (n+1)-th iterates of f at x divided by (1 - K).
|
ContractingWith.toLipschitzWith
theorem ContractingWith.toLipschitzWith :
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → LipschitzWith K f := by
sorry
The theorem "ContractingWith.toLipschitzWith" establishes that for a given function `f` mapping from a type `α` to itself, where `α` is an extended metric space, and for a given nonnegative real number `K`, if `f` is contracting with a contraction constant `K` (i.e., `K` is less than 1 and `f` is Lipschitz continuous with Lipschitz constant `K`), then `f` is also Lipschitz continuous with Lipschitz constant `K`. In other words, any function that contracts distances between points by a constant factor is also Lipschitz continuous.
More concisely: If a function `f` mapping from an extended metric space `α` to itself is contracting with constant `K` (`0 < K <= 1`) and Lipschitz continuous with constant `K`, then `f` is Lipschitz continuous with constant `K`.
|
ContractingWith.exists_fixedPoint
theorem ContractingWith.exists_fixedPoint :
∀ {α : Type u_1} [inst : EMetricSpace α] [cs : CompleteSpace α] {K : NNReal} {f : α → α},
ContractingWith K f →
∀ (x : α),
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)
This theorem, often referred to as Banach's Fixed-Point Theorem or the Contraction Mapping Theorem for `EMetricSpace`, states that for any complete metric space, if there is a contracting map (a map that brings points closer together - specifically, a map `f` such that there exists a nonnegative real `K` with `K` less than `1` for which `f` is Lipschitz continuous with constant `K`), then `f` must have a fixed point. In other words, there exists some point `y` such that when `f` is applied to `y`, the result is `y` itself. Additionally, if the distance from any point `x` to its image under `f` is finite, then the sequence of repeated applications of `f` to `x` will converge to `y`, and the distance from the `n`th term of this sequence to `y` can be bounded by the distance from `x` to `f(x)` times `K` to the power `n` divided by `1 - K`. This theorem is an essential result in analysis and provides the theoretical foundation for many numerical algorithms, such as the method of successive approximations.
More concisely: In a complete metric space, any contracting map (Lipschitz continuous with Lipschitz constant less than 1) has a unique fixed point, and any sequence starting from an arbitrary point converges to it.
|
ContractingWith.isFixedPt_fixedPoint_iterate
theorem ContractingWith.isFixedPt_fixedPoint_iterate :
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} [inst_1 : Nonempty α] [inst_2 : CompleteSpace α]
{n : ℕ} (hf : ContractingWith K f^[n]), Function.IsFixedPt f (ContractingWith.fixedPoint f^[n] hf)
This theorem states that for any natural number `n`, in a nonempty complete metric space `α`, if a function `f : α → α` has a contracting iterate `f^[n]` with constant `K` (a nonnegative real number), then the fixed point of the iterate `f^[n]` is also a fixed point of the original function `f`. In mathematical terms, if `f^n` is a contracting map (meaning it brings points closer together with each iteration), then any point `x` for which `f^n(x) = x` (a fixed point of `f^n`) will also satisfy `f(x) = x` (making it a fixed point of `f` as well).
More concisely: If `f : α → α` is a function on a complete metric space `α` with contracting iterate `f^[n]` having constant `K`, then any fixed point of `f^[n]` is also a fixed point of `f`.
|
ContractingWith.exists_fixedPoint'
theorem ContractingWith.exists_fixedPoint' :
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α},
IsComplete s →
∀ (hsf : Set.MapsTo f s s),
ContractingWith K (Set.MapsTo.restrict f s s hsf) →
∀ {x : α},
x ∈ s →
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)
The Banach fixed-point theorem for maps contracting on a complete subset states that, for a given type `α` with an extended metric space structure, a non-negative real number `K`, a function `f` from `α` to `α`, and a set `s` of `α`, if `s` is complete and the function `f` maps `s` into itself and is contracting on `s`, then for any `x` in `s` where the extended distance between `x` and `f(x)` is not infinite, there exists a `y` in `s` which serves as a fixed point of the function `f`. Furthermore, as `n` goes to infinity, the `n`-th iterate of `f` applied to `x` approaches `y` and the extended distance between the `n`-th iterate of `f` applied to `x` and `y` is less than or equal to the extended distance between `x` and `f(x)` times `K` to the power `n` divided by `1` minus `K`.
More concisely: Given a complete metric space `(α, d)`, a contracting map `f : α → α` on a complete subset `s ⊆ α`, and any `x ∈ s` with finite distance to `f(x)`, there exists a unique fixed point `y ∈ s` such that the distance between `x` and `y` is less than or equal to the distance between `x` and `f(x)` multiplied by `K^n / (1 - K)`, where `K` is the Lipschitz constant of `f` on `s`.
|
ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le'
theorem ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le' :
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
ContractingWith K f →
∀ (g : α → α) {x y : α},
Function.IsFixedPt f x →
Function.IsFixedPt g y → ∀ {C : ℝ}, (∀ (z : α), dist (f z) (g z) ≤ C) → dist x y ≤ C / (1 - ↑K)
The theorem `ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le'` states the following:
Assume that `f` is a contracting map with a contraction constant `K` and `g` is another map that is uniformly `C`-close to `f`. If `x` and `y` are the fixed points of `f` and `g` respectively, then the distance between `x` and `y` is less than or equal to `C / (1 - K)`. In plain English, if two maps are close to each other and both have fixed points, then the distance between these fixed points is bounded by a value that depends on the degree to which the maps are close and the contraction constant of the contracting map.
More concisely: Given contracting maps `f` and `g` with contraction constants `K` and `C`, respectively, if `x` is the fixed point of `f` and `y` is the fixed point of `g`, then `dist(x, y) ≤ C / (1 - K)`.
|
ContractingWith.eq_or_edist_eq_top_of_fixedPoints
theorem ContractingWith.eq_or_edist_eq_top_of_fixedPoints :
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
ContractingWith K f → ∀ {x y : α}, Function.IsFixedPt f x → Function.IsFixedPt f y → x = y ∨ edist x y = ⊤
The theorem `ContractingWith.eq_or_edist_eq_top_of_fixedPoints` states that for any type `α` equipped with an extended metric space structure, any nonnegative real `K`, and any function `f` from `α` to `α`, if `f` is contracting with `K` (meaning `K` is less than 1 and `f` is Lipschitz with `K`), then for any two points `x` and `y` in `α` that are fixed points of `f` (meaning `f(x)` equals `x` and `f(y)` equals `y`), either `x` is equal to `y` or the extended distance between `x` and `y` is infinite. This theorem essentially states that a contracting function in an extended metric space can have at most one fixed point, unless there are points infinitely far apart.
More concisely: In an extended metric space, a contracting function with Lipschitz constant less than 1 has at most one fixed point, or all fixed points are infinitely far apart.
|
ContractingWith.efixedPoint_eq_of_edist_lt_top'
theorem ContractingWith.efixedPoint_eq_of_edist_lt_top' :
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
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) ≠ ⊤),
edist x y ≠ ⊤ →
ContractingWith.efixedPoint' f hsc hsf hfs x hxs hx = ContractingWith.efixedPoint' f htc htf hft y hyt hy
This theorem states that, given a global contracting map `f` and two complete forward-invariant sets `s` and `t`, if a point `x` in `s` and a point `y` in `t` are at a finite distance from each other, then the unique fixed point derived from `x` in set `s` (`efixedPoint'`) is the same as the unique fixed point derived from `y` in set `t` (`efixedPoint'`). The theorem also takes into account additional conditions that `f` contracts on both sets `s` and `t`. This flexibility allows it to prove the desired equality even with non-trivial proofs of these conditions.
More concisely: Given a global contracting map `f` and complete forward-invariant sets `s` and `t` such that `f` contracts on both sets and any two points `x` in `s` and `y` in `t` are at a finite distance, the unique fixed points in `s` and `t` are equal.
|
ContractingWith.fixedPoint_isFixedPt
theorem ContractingWith.fixedPoint_isFixedPt :
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
[inst_2 : CompleteSpace α], Function.IsFixedPt f (ContractingWith.fixedPoint f hf)
The theorem `ContractingWith.fixedPoint_isFixedPt` states that for any type `α` which is a metric space and any function `f` from `α` to `α` that is contracting with a non-negative real number `K`, given that `α` is nonempty and a complete space, the point provided by the function `ContractingWith.fixedPoint` is actually a fixed point of `f`. In other words, if `f` is a contracting function in a nonempty complete metric space, then the point determined by `ContractingWith.fixedPoint` satisfies the property that `f` of this point equals the point itself.
More concisely: If `α` is a nonempty complete metric space and `f: α → α` is a contracting function with constant `K`, then the point returned by `ContractingWith.fixedPoint f` is a fixed point of `f`, i.e., `f (ContractingWith.fixedPoint f) = ContractingWith.fixedPoint f`.
|
ContractingWith.one_sub_K_pos
theorem ContractingWith.one_sub_K_pos :
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → 0 < 1 - ↑K
This theorem states that for any type `α` that is a metric space, and for any nonnegative real number `K` and function `f` from `α` to `α`, if `f` is a contracting map with constant `K` (meaning `K` is less than `1` and `f` is `K`-Lipschitz), then the value `1 - K` is always positive. In other words, the difference between `1` and the Lipschitz constant of a contracting map is always greater than `0`.
More concisely: For any metric space `α` and contracting map `f:` `α` `->` `α` with Lipschitz constant `K` < 1, `1 - K` is positive.
|
ContractingWith.one_sub_K_ne_zero
theorem ContractingWith.one_sub_K_ne_zero :
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → 1 - ↑K ≠ 0
The theorem `ContractingWith.one_sub_K_ne_zero` states that for any type `α` equipped with an extended metric space structure, any nonnegative real number `K`, and any function `f` from `α` to `α` that is `ContractingWith K`, the real number `1 - K` is not equal to zero. This essentially means that if `f` is a contracting map with a contraction factor `K` (where `K` is less than 1), then `1 - K` will never be zero. This prevents the contraction factor from being 1, which would cause the distance between `f(x)` and `f(y)` to be the same as the distance between `x` and `y`, contradicting the property of a contracting map.
More concisely: For any type with an extended metric space structure, if `f` is a contracting function with contraction factor `K` (`0 < K < 1`), then `1 - K` is not equal to zero.
|