From 670ee10b271185104e99ccdcab7d9b96cbec0ff4 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Wed, 20 Apr 2016 14:31:07 -0400
Subject: [PATCH] feat(library/analysis): basic properties about real
 derivatives

---
 .../analysis/bounded_linear_operator.lean     |  4 +-
 library/theories/analysis/metric_space.lean   | 89 +++++++++++++------
 library/theories/analysis/real_deriv.lean     | 60 +++++++++++++
 library/theories/analysis/real_limit.lean     |  8 ++
 4 files changed, 132 insertions(+), 29 deletions(-)
 create mode 100644 library/theories/analysis/real_deriv.lean

diff --git a/library/theories/analysis/bounded_linear_operator.lean b/library/theories/analysis/bounded_linear_operator.lean
index dc8aa7b17..924e9d8ef 100644
--- a/library/theories/analysis/bounded_linear_operator.lean
+++ b/library/theories/analysis/bounded_linear_operator.lean
@@ -17,7 +17,7 @@ structure is_bdd_linear_map [class] {V W : Type} [normed_vector_space V] [normed
           extends is_module_hom ℝ f :=
   (op_norm : ℝ) (op_norm_pos : op_norm > 0) (op_norm_bound : ∀ v : V, ∥f v∥ ≤ op_norm * ∥v∥)
 
-theorem is_bdd_linear_map_id (V : Type) [normed_vector_space V] : is_bdd_linear_map (λ x : V, x) :=
+theorem is_bdd_linear_map_id [instance] (V : Type) [normed_vector_space V] : is_bdd_linear_map (λ x : V, x) :=
   begin
     fapply is_bdd_linear_map.mk,
     repeat (intros; reflexivity),
@@ -218,7 +218,7 @@ theorem frechet_deriv_spec [Hf : frechet_diffable_at f x] :
         (λ h : V, ∥f (x + h) - f x - (frechet_deriv_at f x h) ∥ / ∥ h ∥) ⟶ 0 at 0 :=
   frechet_diffable_at.is_fr_der _ _ f x
 
-theorem frechet_deriv_at_const {w : W} : is_frechet_deriv_at (λ v : V, w) (λ v : V, 0) x :=
+theorem frechet_deriv_at_const (w : W) : is_frechet_deriv_at (λ v : V, w) (λ v : V, 0) x :=
   begin
     intros ε Hε,
     existsi 1,
diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean
index 7d49a14a8..0bf37e813 100644
--- a/library/theories/analysis/metric_space.lean
+++ b/library/theories/analysis/metric_space.lean
@@ -347,6 +347,7 @@ have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrit
 by rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H
 -/
 
+--<<<<<<< HEAD
 proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at ∞]) :
             ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K :=
   have eventually (λ n, dist (X n) x < 1) [at ∞],
@@ -362,6 +363,66 @@ proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at 
       else
         show dist (X n) x ≤ K,
           from le.trans (le_of_lt (HN n (le_of_not_gt Hn))) !le_max_left)
+--=======
+/-proposition converges_to_seq_of_converges_to_seq_offset_succ
+    {X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y in ℕ) :
+  X ⟶ y in ℕ :=
+@converges_to_seq_of_converges_to_seq_offset M _ X y 1 H
+
+proposition converges_to_seq_offset_iff (X : ℕ → M) (y : M) (k : ℕ) :
+  ((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
+iff.intro converges_to_seq_of_converges_to_seq_offset !converges_to_seq_offset
+
+proposition converges_to_seq_offset_left_iff (X : ℕ → M) (y : M) (k : ℕ) :
+  ((λ n, X (k + n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
+iff.intro converges_to_seq_of_converges_to_seq_offset_left !converges_to_seq_offset_left
+
+proposition converges_to_seq_offset_succ_iff (X : ℕ → M) (y : M) :
+  ((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
+iff.intro converges_to_seq_of_converges_to_seq_offset_succ !converges_to_seq_offset_succ
+
+section
+open list
+private definition r_trans : transitive (@le ℝ _) := λ a b c, !le.trans
+private definition r_refl : reflexive (@le ℝ _) := λ a, !le.refl
+
+proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ) :
+            ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K :=
+  begin
+    cases H zero_lt_one with N HN,
+    cases em (N = 0),
+    existsi 1,
+    intro n,
+    apply le_of_lt,
+    apply HN,
+    rewrite a,
+    apply zero_le,
+    let l := map (λ n : ℕ, -dist (X n) x) (upto N),
+    have Hnenil : l ≠ nil, from (map_ne_nil_of_ne_nil _ (upto_ne_nil_of_ne_zero a)),
+    existsi max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1,
+    intro n,
+    have Hsmn : ∀ m : ℕ, m < N → dist (X m) x ≤ max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, begin
+      intro m Hm,
+      apply le.trans,
+      rotate 1,
+      apply le_max_left,
+      note Hall := min_lemma real.le_total r_trans r_refl Hnenil,
+      have Hmem : -dist (X m) x ∈ (map (λ (n : ℕ), -dist (X n) x) (upto N)), from mem_map _ (mem_upto_of_lt Hm),
+      note Hallm' := of_mem_of_all Hmem Hall,
+      apply le_neg_of_le_neg,
+      exact Hallm'
+    end,
+    cases em (n < N) with Elt Ege,
+    apply Hsmn,
+    exact Elt,
+    apply le_of_lt,
+    apply lt_of_lt_of_le,
+    apply HN,
+    apply le_of_not_gt Ege,
+    apply le_max_right
+  end
+end
+>>>>>>> feat(library/analysis): basic properties about real derivatives-/
 
 /- cauchy sequences -/
 
@@ -552,32 +613,6 @@ variables {M N : Type} [Hm : metric_space M] [Hn : metric_space N]
 include Hm Hn
 open topology set
 
-/-  begin
-    intros x Hx ε Hε,
-    rewrite [↑continuous_on at Hfs],
-    cases @Hfs (open_ball (f x) ε) !open_ball_open with t Ht,
-    cases Ht with Ht Htx,
-
-    cases @Hfx (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with V HV,
-    cases HV with HV HVx,
-    cases HVx with HVx HVf,
-    cases ex_Open_ball_subset_of_Open_of_nonempty HV HVx with δ Hδ,
-    cases Hδ with Hδ Hδx,
-    existsi δ,
-    split,
-    exact Hδ,
-    intro x' Hx',
-    rewrite dist_comm,
-    apply and.right,
-    apply HVf,
-    apply Hδx,
-    apply and.intro !mem_univ,
-    rewrite dist_comm,
-    apply Hx',
-  end-/
-
-/- continuity at a point -/
-
 -- the ε - δ definition of continuity is equivalent to the topological definition
 theorem continuous_at_intro {f : M → N} {x : M}
         (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) :
@@ -726,7 +761,7 @@ approaches_at_intro
 --definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x
 
 theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converges_seq X] {f : M → N}
-                                         (Hf : continuous f) :
+        (Hf : continuous f) :
         converges_seq (λ n, f (X n)) :=
   begin
     cases HX with xlim Hxlim,
diff --git a/library/theories/analysis/real_deriv.lean b/library/theories/analysis/real_deriv.lean
new file mode 100644
index 000000000..0f86d65fa
--- /dev/null
+++ b/library/theories/analysis/real_deriv.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2016 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Robert Y. Lewis
+
+Derivatives on ℝ
+-/
+import .bounded_linear_operator
+open real nat classical topology analysis
+noncomputable theory
+
+namespace real
+
+-- move this to group
+theorem add_sub_self (a b : ℝ) : a + b - a = b :=
+  by rewrite [add_sub_assoc, add.comm, sub_add_cancel]
+
+-- make instance of const mul bdd lin op?
+
+definition derivative_at (f : ℝ → ℝ) (d x : ℝ) := is_frechet_deriv_at f (λ t, d • t) x
+
+theorem derivative_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + h) - f x) / h) ⟶ d at 0) :
+        derivative_at f d x :=
+  begin
+    apply is_frechet_deriv_at_intro,
+    intros ε Hε,
+    cases H Hε with δ Hδ,
+    existsi δ,
+    split,
+    exact and.left Hδ,
+    intro y Hy,
+    rewrite [-sub_zero y at Hy{2}],
+    note Hδ' := and.right Hδ y Hy,
+    have Hδ'' : abs ((f (x + y) - f x - d * y) / y) < ε,
+      by rewrite [-div_sub_div_same, mul_div_cancel _ (and.left Hy)]; apply Hδ',
+    show abs (f (x + y) - f x - d * y) / abs y < ε, by rewrite -abs_div; apply Hδ''
+  end
+
+theorem deriv_at_const (c x : ℝ) : derivative_at (λ t, c) 0 x :=
+  begin
+    apply derivative_at_intro,
+    have (λ h, (c - c) / h) = (λ h, 0), from funext (λ h, by rewrite [sub_self, zero_div]),
+    rewrite this,
+    apply converges_to_at_constant
+  end
+
+theorem deriv_at_id (x : ℝ) : derivative_at (λ t, t) 1 x :=
+  begin
+    apply derivative_at_intro,
+    apply converges_to_at_real_intro,
+    intros ε Hε,
+    existsi 1,
+    split,
+    exact zero_lt_one,
+    intros x' Hx',
+    rewrite [add_sub_self, div_self (and.left Hx'), sub_self, abs_zero],
+    exact Hε
+  end
+
+end real
diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean
index 36c0656d5..03200a652 100644
--- a/library/theories/analysis/real_limit.lean
+++ b/library/theories/analysis/real_limit.lean
@@ -405,7 +405,15 @@ section limit_operations_continuous
 variables {f g h : ℝ → ℝ}
 variables {a b x y : ℝ}
 
+--<<<<<<< HEAD
 theorem mul_converges_to_at (Hf : f ⟶ a [at x]) (Hg : g ⟶ b [at x]) : (λ z, f z * g z) ⟶ a * b [at x] :=
+/-=======
+theorem converges_to_at_real_intro (Hf : ∀ ⦃ε⦄, ε > 0 →
+        (∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ abs (x' - x) < δ → abs (f x' - y) < ε)) :
+        converges_to_at f y x := Hf
+
+theorem mul_converges_to_at (Hf : f ⟶ a at x) (Hg : g ⟶ b at x) : (λ z, f z * g z) ⟶ a * b at x :=
+>>>>>>> feat(library/analysis): basic properties about real derivatives-/
   begin
     apply converges_to_at_of_all_conv_seqs,
     intro X HX,