## Stream: maths

### Topic: fixed point API

#### Patrick Massot (Mar 04 2019 at 22:17):

Building on Sébastien's https://github.com/leanprover-community/mathlib/pull/788 I propose an API for the Banach fixed point theorem that would look like:

namespace metric
variables {α : Type*} [metric_space α] [inhabited α] [complete_space α]
open metric filter
def fixed_point (f : α → α) : α := lim (map (λ n, f^[n] \$ default α) at_top)

lemma fixed_point_fixed {K : ℝ} (hK : K < 1) {f : α → α} (hf : lipschitz_with K f) :
f (fixed_point f) = fixed_point f :=
let x₀ := default α in
have cauchy_seq (λ n, f^[n] x₀) := begin
refine cauchy_seq_of_le_geometric K (dist x₀ (f x₀)) hK (λn, _),
rw [nat.iterate_succ f n x₀, mul_comm],
exact and.right (hf.iterate n) x₀ (f x₀)
end,
let ⟨x, hx⟩ := cauchy_seq_tendsto_of_complete this in
have fxx : f x = x,
from fixed_point_of_tendsto_iterate (hf.to_uniform_continuous.continuous.tendsto x) ⟨x₀, hx⟩,
begin
dsimp [fixed_point],
exact tendsto_nhds_unique filter.at_top_ne_bot hx (lim_spec ⟨x, hx⟩) ▸ fxx,
end

lemma fixed_point_spec {K : ℝ} (hK : K < 1) {f : α → α} (hf : lipschitz_with K f) :
∀ x, (f x = x) ↔ x = fixed_point f :=
λ x, ⟨λ h, lipschitz_with.fixed_point_unique_of_contraction hK hf h (fixed_point_fixed hK hf),
λ h, eq.symm h ▸ fixed_point_fixed hK hf⟩

end metric


What do you think? Do you have nicer names? Nicer proofs? An even better API?

#### Patrick Massot (Mar 04 2019 at 22:45):

Sample use (which motivated this API):

section
open metric
variables {E : Type*} [banach_space ℝ E]

lemma lipschitz_with_translate {K : ℝ} {u : E → E} (hu : lipschitz_with K u) (v : E) :
lipschitz_with K (λ x, v + u x) :=
⟨hu.1, λ x x',
calc dist (v + u x) (v + u x') ≤ ∥(v + u x) - (v + u x')∥ : by rw dist_eq_norm
... = ∥u x - u x'∥        : by simp
... =  dist (u x) (u x')  : by rw ← dist_eq_norm
... ≤ K*dist x x'         : hu.2 _ _⟩

/-- The inverse of id - u -/
def lipschitz_global_inverse (u : E → E) : E → E := λ y, fixed_point (λ x, y + u x)
end

namespace lipschitz_global_inverse
open function lipschitz_with classical metric
variables {E : Type*} [banach_space ℝ E]

variables {K : ℝ} (hK : K < 1) {u : E → E} (hu : lipschitz_with K u)
include hK hu

lemma is_inverse : function.inverse (id - u) (lipschitz_global_inverse u) :=
begin
rw ← inverse_iff,
intros x y,
let w := fixed_point (λ z, x + u z),
have : x + u y = y ↔ y = w,
from fixed_point_spec hK (lipschitz_with_translate hu x) y,
change w = y ↔ x = y - u y,
split ; intro h,
{ exact eq_sub_of_add_eq  (this.2 h.symm) },
{ rw h at this, simp at this, exact this.symm }
end
end lipschitz_global_inverse


#### Chris Hughes (Mar 04 2019 at 22:52):

fixed_point_spec should be called either fixed_point_unique or apply_eq_self_iff_eq_fixed_point

#### Sebastien Gouezel (Mar 05 2019 at 08:44):

You should define fixed_point in a more general setting, removing all the type classes except nonempty α and choosing a fixed point if there is one and something arbitrary otherwise (using epsilon). This definition will be useful in many different settings!

#### Patrick Massot (Mar 05 2019 at 08:45):

I was also thinking this in my bed last night. I'll try it

#### Patrick Massot (Mar 05 2019 at 08:58):

open classical
variables {α : Type*} [nonempty α]

def fixed_point (f : α → α) : α := epsilon (λ x, f x = x)

def fixed_point_spec {f : α → α} {x : α} (h : f x = x) : f (fixed_point f) = fixed_point f :=
epsilon_spec ⟨x, h⟩


Done

#### Patrick Massot (Mar 05 2019 at 08:59):

And it works even better in the application to Banach fixed point

Last updated: May 10 2021 at 08:14 UTC