/-
Copyright (c) 2022 Clara Löh. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.txt.
Author: Clara Löh.
-/

import tactic                      -- standard proof tactics
import topology.metric_space.basic -- basics on metric spaces

open classical  -- we work in classical logic

/-
We define quasi-isometries as quasi-isometric embeddings 
that admit a quasi-inverse quasi-isometric embedding. 

Similarly, we define isometries between metric spaces 
and show that isometries are quasi-isometries.
-/

/-
# Quasi-isometric embeddings and quasi-isometries
-/

-- quasi-isometric embeddings
def is_QIE_lower
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f : X → Y)
    (c b : ℝ)
:= ∀ x x' : X, dist (f x) (f x') ≥ 1/c * dist x x' - b    

def is_QIE_upper
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f : X → Y)
    (c b : ℝ)
:= ∀ x x' : X, dist (f x) (f x') ≤ c * dist x x' + b    

def is_QIE' 
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f : X → Y)
    (c b : ℝ)
:= is_QIE_upper f c b 
 ∧ is_QIE_lower f c b 

def is_QIE 
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f : X → Y)
:= ∃ c : ℝ, ∃ b : ℝ,
   c > 0 
 ∧ b > 0
 ∧ is_QIE' f c b 


-- finite distance
def has_fin_dist' 
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f g : X → Y)
    (c : ℝ)
:= ∀ x : X, dist (f x) (g x) ≤ c    

def has_fin_dist 
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f g : X → Y)
:= ∃ c : ℝ, 
   c > 0
 ∧ has_fin_dist' f g c

def are_quasi_inverse 
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f : X → Y)
    (g : Y → X)
:= has_fin_dist (g ∘ f) id
 ∧ has_fin_dist (f ∘ g) id 

-- quasi-isometry
def is_QI 
    {X Y : Type*} [metric_space X] [metric_space Y]
    (f : X → Y)
:= is_QIE f
 ∧ ∃ g : Y → X, is_QIE g 
              ∧ are_quasi_inverse f g

/-
# Isometric embeddings and isometries
-/

-- definition of isometries
def is_isometry 
     {X Y : Type*} [metric_space X] [metric_space Y]
     (f : X → Y)
:= sorry 
-- Exercise: complete this definition;
-- keeping the definition structurally close to the QI case 
-- will make the proof of the theorem below easier

-- Exercise: it could be helpful to prove individual steps 
-- of the main proof in separate lemmas

-- Every isometry is a quasi-isometry
theorem isometries_are_quasiisometries 
-- Exercise: complete the statement of the theorem
:=
begin
  -- Exercise: complete the proof of the theorem
end