fixed point API

Stream: maths

[Patrick Massot]

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]

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]

fixed_point_spec should be called either fixed_point_unique or apply_eq_self_iff_eq_fixed_point

[Sebastien Gouezel]

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]

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

[Patrick Massot]

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]

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