out_param_hell.lean

/-
Copyright (c) 2019 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Banach spaces.

Authors: Patrick Massot
-/
import analysis.normed_space.basic topology.uniform_space.basic topology.metric_space.lipschitz
import analysis.specific_limits
import logic.function

noncomputable theory


section
open filter
variables (α : out_param $ Type*) (β : Type*) [out_param $ normed_field α]

class banach_space extends normed_space α β :=
[complete : complete_space β]

attribute [instance] banach_space.complete

instance real.banach_space : banach_space ℝ ℝ :=
{ ..normed_field.to_normed_space }
end

instance inhabited_vector_space {k : Type*} {α : Type*}
  [discrete_field k] [add_comm_group α] [vector_space k α] : inhabited α := ⟨0⟩

section function
open function

def function.inverse {α : Type*} {β : Type*} (g : β → α) (f : α → β) :=
left_inverse g f ∧ right_inverse g f

lemma inverse_iff {α : Type*} {β : Type*} (f : α → β) (g : β → α) :
  (∀ a b, f a = b ↔ a = g b) ↔ function.inverse g f :=
⟨assume h, ⟨λ a, eq.symm $ (h a $ f a).1 rfl, λ b, (h (g b)  b).2 rfl⟩,
 assume ⟨hl, hr⟩ a b, ⟨λ h, hl a ▸ congr_arg g h, λ h, eq.symm (congr_arg f h) ▸ (hr b)⟩⟩
end function

section fixed_point
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⟩
end fixed_point

namespace metric
variables {α : Type*} [metric_space α] [inhabited α] [complete_space α]
open metric filter classical

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⟩,
fixed_point_spec fxx

lemma fixed_point_iff {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

section
open metric
variables {α : out_param $ Type*} [out_param $ normed_field α]
variables {E : Type*} [B : banach_space α E]
include B

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` when `u` is contracting -/
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 {α : Type*} [normed_field α]
variables {E : Type*} [B : banach_space α E]
include B

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) :=
-- (@lipschitz_global_inverse α _ E _ 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_iff 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