Zulip Chat Archive

Stream: maths

Topic: fixed point API

view this post on Zulip 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₀)
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,
  dsimp [fixed_point],
  exact tendsto_nhds_unique filter.at_top_ne_bot hx (lim_spec x, hx)  fxx,

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?

view this post on Zulip Patrick Massot (Mar 04 2019 at 22:45):

Sample use (which motivated this API):

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)

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) :=
  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 lipschitz_global_inverse

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Patrick Massot (Mar 05 2019 at 08:45):

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

view this post on Zulip 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


view this post on Zulip 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