lip_extends.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 metric
variables {α : Type*} [metric_space α]
lemma metric.nonneg_of_mem_closed_ball {a x : α} {r : ℝ} (h : x ∈ closed_ball a r) : 0 ≤ r :=
by rw mem_closed_ball at h ; exact le_trans dist_nonneg h
end

section lipschitz_on_with
open set
variables {α : Type*} {β : Type*} [metric_space α] [metric_space β]

def lipschitz_on_with (s : set α) (K : ℝ) (f : α → β) :=
0 ≤ K ∧ ∀x y ∈ s, dist (f x) (f y) ≤ K * dist x y

example (K : ℝ) (f : α → β) : lipschitz_with K f ↔ lipschitz_on_with univ K f :=
⟨λ ⟨hK, h⟩, ⟨hK, λ x y _ _, h x y⟩, λ ⟨hK, h⟩,  ⟨hK, λ x y, h x y (mem_univ x) (mem_univ y)⟩⟩
end lipschitz_on_with

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

def rho (a : E) (r : ℝ) : E → E :=
λ x, if ∥x -a∥ ≤ r then x else a + (r/∥x - a∥)•(x-a)
local notation `ρ` := rho


lemma rho_norm (a x: E) {r : ℝ} (hr : 0 ≤ r) (hx : r ≤ ∥x-a∥) : ∥ ρ a r x - a∥ = r :=
begin
  cases lt_or_eq_of_le hx,
  { have Rx : ρ a r x = a + (r/∥x - a∥)•(x-a), from if_neg (not_le_of_lt h),
    calc
    ∥ ρ a r x - a∥ = ∥ a + (r/∥x - a∥)•(x-a) - a∥ : by rw Rx
    ... = ∥(r/∥x - a∥)•(x-a)∥ : by rw [add_comm, add_sub_assoc, sub_self, add_zero]
    ... = _ : by {rw[norm_smul, norm_div, norm_norm, div_mul_cancel, real.norm_eq_abs, abs_of_nonneg hr],
                  apply ne_of_gt, linarith } },
  rw [show ρ a r x = x, from if_pos (le_of_eq h.symm), h],
end

lemma rho_ball (a x: E) {r : ℝ} (hr : 0 ≤ r) : ρ a r x ∈ closed_ball a r :=
begin
  rw [mem_closed_ball, dist_eq_norm],
  by_cases h : r ≤ ∥x - a∥,
  { exact le_of_eq (rho_norm _  _ hr h) },
  { rw not_le at h,
    replace h := le_of_lt h,
    rw show ρ a r x = x, from if_pos h,
    exact h }
end

lemma lipschitz_rho_aux₁ {r₁ r₂ : ℝ} {a y : E} (h₁ : 0 ≤ r₁) (h₂ : r₁ ≤ r₂) (hy : r₂ ≤ ∥y-a∥) :
  ρ a r₁ (ρ a r₂ y) = ρ a r₁ y :=
begin
  set R₁ := ρ a r₁,
  set R₂ := ρ a r₂,
  cases lt_or_eq_of_le hy with hy' hy',
  { cases lt_or_eq_of_le h₂ with h₂' h₂',
    { clear hy,
      have : ∥R₂ y - a∥ = r₂, from rho_norm _ _ (le_trans h₁ h₂) (le_of_lt hy'),
      rw [show R₁ (R₂ y) = _, from if_neg $ by linarith],
      rw this,
      rw [show R₂ y = _, from if_neg $ not_le_of_lt hy'],
      rw [show R₁ y = _, from if_neg $ by linarith],
      rw [show a + (r₂ / ∥y - a∥) • (y - a) - a = (r₂ / ∥y - a∥) • (y - a), by abel],
      rw smul_smul,
      rw field.div_mul_div_cancel ; apply ne_of_gt ; linarith },
    { have : ∥R₂ y - a∥ = r₂, from rho_norm _ _ (le_trans h₁ h₂) (le_of_lt hy'),
      rw ← h₂' at this,
      rw [show R₁ (_ ) = _, from if_pos _],
      simp [R₁, R₂, h₂'],
      rw ← this }},
  { rw [show R₂ y = _, from if_pos $ le_of_eq hy'.symm] },
end

lemma lipschitz_rho_aux₂ {r : ℝ} {a x y : E} (hx : ∥x - a∥ ≤ r) (hy : r ≤ ∥y-a∥) :
  ∥y - ρ a r y∥ ≤ ∥x - y∥ :=
begin
  cases lt_or_eq_of_le hy with h h,
  { set R := ρ a r,
    have Rx : R x = x, from if_pos hx,
    have Ry : R y = a + (r/∥y - a∥)•(y-a), from if_neg (not_le_of_lt h),
    have hya : ∥y - a∥ > 0, by linarith using [norm_nonneg (x-a)],
    have ineq : abs (1 - r/∥y - a∥) = 1 - r/∥y - a∥,
    { apply abs_of_nonneg,
      apply le_of_mul_le_mul_left _ hya,
      rw [mul_zero, mul_sub, mul_one, mul_div_cancel'],
      linarith,
      exact ne_of_gt hya},
    calc
      ∥y - R y∥ = ∥y - (a + (r/∥y - a∥)•(y-a))∥ : by rw Ry
          ...   =  ∥(1 : ℝ)•(y - a) - (r/∥y - a∥)•(y-a)∥ : by simp
          ...   =  ∥(1 - r/∥y - a∥)•(y-a)∥ : by rw ←sub_smul
          ...   = (1 - r/∥y - a∥)*∥y-a∥ : by rw [norm_smul, real.norm_eq_abs, ineq]
          ...   = ∥y - a∥ - r : by rw [sub_mul, one_mul, div_mul_cancel] ; exact ne_of_gt hya
          ...   = ∥(y-x) + (x-a)∥ - r : by congr' 2 ; abel
          ...   ≤ ∥y-x∥ + ∥x-a∥ - r : sub_le_sub (norm_triangle _ _) (le_refl r)
          ...   = ∥y-x∥ + (∥x-a∥ - r) : add_sub_assoc _ _ _
          ...   ≤  ∥y-x∥ + 0 : add_le_add (le_refl _) (by linarith)
          ...   =  ∥x - y∥  : by rw [add_zero, norm_sub_rev] },
  { rw [show ρ a r y = y, from if_pos (le_of_eq h.symm)],
    simp [norm_nonneg] }
end

lemma lipschitz_rho_aux₃ {r : ℝ} {a x y : E} (hr : 0 ≤ r) (h : ∥x - a∥ = ∥y - a∥) :
  ∥ρ a r x - ρ a r y∥ ≤ ∥x - y∥ :=
begin
  set R := ρ a r,
  set r' := ∥x - a∥,
  by_cases hx : ∥x - a∥ ≤ r,
  { have hy : ∥y - a∥ ≤ r, from h ▸ hx,
    simp [show R x = x, from if_pos hx, show R y = y, from if_pos hy] },
  { have hy : ¬ ∥y - a∥ ≤ r, from h ▸ hx,
    have Rx : R x = a + (r/r')•(x-a), from if_neg hx,
    have Ry : R y = a + (r/r')•(y-a), from h.symm ▸ if_neg hy,
    rw [Rx, Ry],
    set τ := r/r',
    have tauone : abs τ ≤ 1,
    { rw ← h at hy,
      have : 0 < r', by linarith,
      have tau_noneng : 0 ≤ τ := div_nonneg hr (by linarith),
      rw abs_of_nonneg tau_noneng,
      apply le_of_mul_le_mul_left _ this,
      simp [τ],
      rw mul_div_cancel', linarith, exact ne_of_gt this },
    calc ∥a + τ • (x - a) - (a + τ • (y - a))∥ =
     ∥τ • (x - a) - τ • (y - a)∥ : by congr' 1 ; abel
     ... = abs (τ) * ∥(x-a) - (y -a)∥ : by rw [←smul_sub, norm_smul, real.norm_eq_abs]
     ... = abs (τ) * ∥x - y∥ : by rw show (x-a)-(y-a) = x-y, by abel
     ... ≤ 1*∥x - y∥ : mul_le_mul tauone (le_refl _) (norm_nonneg _) (by norm_num)
     ... = ∥x - y∥ : one_mul _,
  }
end

lemma lipschitz_rho (a : E) (r : ℝ) (hr : 0 ≤ r): lipschitz_with 2 (ρ a r) :=
⟨by norm_num, begin
  intros x y,
  set R := ρ a r,
  repeat { rw dist_eq_norm },
  wlog h : ∥x - a∥ ≤ ∥y - a∥ using x y,
  { by_cases hy : ∥y - a∥ ≤ r,
    { have hx : ∥x - a∥ ≤ r, from le_trans h hy, clear h,
      rw [show R x = x, from if_pos hx, show R y = y, from if_pos hy],
      have := norm_nonneg (x - y),
      linarith },
    { by_cases hx : ∥x - a∥ ≤ r,
      { have : ∥y - R y∥ ≤ ∥x - y∥ := lipschitz_rho_aux₂ hx (by linarith),
        have Rx : R x = x, from if_pos hx,
        calc ∥R x - R y∥ = ∥(x - y) + (y - R y)∥ : by simp[Rx]
        ... ≤ ∥x - y∥ + ∥y - R y∥ : norm_triangle _ _
        ... ≤ 2*∥x -y ∥ : by linarith,
       },
      { have Rx : R x = a + (r/∥x - a∥)•(x-a), from if_neg hx,
        have Ry : R y = a + (r/∥y - a∥)•(y-a), from if_neg hy,
        rw not_le at *,
        set r₁ := ∥x - a∥,
        let R₁ := ρ a r₁,
        have eq1 : R y = R (R₁ y),
        { refine eq.symm (lipschitz_rho_aux₁ hr _ _) ;
          linarith },
        have eq2 : ∥R₁ y - a∥ = r₁,
        by apply rho_norm ; linarith,

        have ineq' : ∥y - R₁ y∥ ≤ ∥x - y∥,
          from lipschitz_rho_aux₂ (le_refl _) h,
        calc ∥R x - R y∥ = ∥R x - R (R₁ y)∥ : by rw eq1
        ... ≤ ∥x - R₁ y∥ : lipschitz_rho_aux₃ hr eq2.symm
        ... = ∥(x - y) + (y - R₁ y)∥ : by abel
        ... ≤ ∥x - y∥ + ∥y - R₁ y∥ : norm_triangle _ _
        ... ≤ ∥x - y∥ + ∥x - y∥ : add_le_add (le_refl _) ineq'
        ... = 2*∥x - y∥ : by ring } } },
  { rwa [norm_sub_rev x y, norm_sub_rev (R x) (R y)] }
end⟩

variables {F : Type*} [normed_space ℝ F]
lemma lipschitz_extend_from_ball {a : E} {r : ℝ} {K : ℝ} {f : E → F}
(h : lipschitz_on_with (closed_ball a r) K f):
∃ g : E → F, (∀ x ∈ closed_ball a r, g x = f x) ∧ lipschitz_with (2*K) g :=
begin
  by_cases hr : 0 ≤ r,
  { set R := ρ a r,
    use f ∘ R,
    split,
    { intros x x_in,
      rw function.comp_app,
      congr' 1,
      rw [mem_closed_ball, dist_eq_norm] at x_in,
      rw show R x = x, from if_pos x_in },
    { cases h with Knonneg h,
      refine ⟨by linarith, _⟩,
      intros x y,
      specialize h (R x) (R y) (rho_ball a _ hr) (rho_ball a _ hr),
      have : dist (R x) (R y) ≤ 2*dist x y, from (lipschitz_rho _ _ hr).2 _ _,
      calc dist ((f ∘ R) x) ((f ∘ R) y) = dist (f $ R x) (f $ R y) : rfl
      ... ≤ K*dist (R x) (R y) : h
      ... ≤ K*(2*dist x y) : mul_le_mul (le_refl _) this dist_nonneg Knonneg
      ... = 2*K*dist x y : by ring } },
  { use (λ e, 0),
    split,
    { intros x x_in,
      exfalso,
      exact hr (nonneg_of_mem_closed_ball x_in) },
    { replace h := h.1,
      refine ⟨by linarith, λ x y, _⟩,
      have := @dist_nonneg _ _ x y,
      suffices : 0*0*0 ≤ 2 * K * dist x y, by simpa using this,
      apply mul_le_mul; simp ; linarith } }
end