feat(analysis/complex/exponential): derivatives

src/analysis/asymptotics.lean

@@ -755,13 +755,13 @@ end
 end
 
 section
-variables [normed_field β]
+variables {K : Type*} [normed_field K]
 
-theorem tendsto_nhds_zero_of_is_o {f g : α → β} {l : filter α} (h : is_o f g l) :
+theorem tendsto_nhds_zero_of_is_o {f g : α → K} {l : filter α} (h : is_o f g l) :
   tendsto (λ x, f x / (g x)) l (𝓝 0) :=
 have eq₁ : is_o (λ x, f x / g x) (λ x, g x / g x) l,
   from is_o_mul_right h (is_O_refl _ _),
-have eq₂ : is_O (λ x, g x / g x) (λ x, (1 : β)) l,
+have eq₂ : is_O (λ x, g x / g x) (λ x, (1 : K)) l,
   begin
     use [1, zero_lt_one],
     filter_upwards [univ_mem_sets], simp,
@@ -771,10 +771,10 @@ have eq₂ : is_O (λ x, g x / g x) (λ x, (1 : β)) l,
   end,
 is_o_one_iff.mp (eq₁.trans_is_O eq₂)
 
-private theorem is_o_of_tendsto {f g : α → β} {l : filter α}
+private theorem is_o_of_tendsto {f g : α → K} {l : filter α}
     (hgf : ∀ x, g x = 0 → f x = 0) (h : tendsto (λ x, f x / (g x)) l (𝓝 0)) :
   is_o f g l :=
-have eq₁ : is_o (λ x, f x / (g x)) (λ x, (1 : β)) l,
+have eq₁ : is_o (λ x, f x / (g x)) (λ x, (1 : K)) l,
   from is_o_one_iff.mpr h,
 have eq₂ : is_o (λ x, f x / g x * g x) g l,
   by convert is_o_mul_right eq₁ (is_O_refl _ _); simp,
@@ -789,11 +789,32 @@ have eq₃ : is_O f (λ x, f x / g x * g x) l,
   end,
 eq₃.trans_is_o eq₂
 
-theorem is_o_iff_tendsto {f g : α → β} {l : filter α}
+theorem is_o_iff_tendsto {f g : α → K} {l : filter α}
     (hgf : ∀ x, g x = 0 → f x = 0) :
   is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0) :=
 iff.intro tendsto_nhds_zero_of_is_o (is_o_of_tendsto hgf)
 
+theorem is_o_pow_pow {m n : ℕ} (h : m < n) :
+  is_o (λ(x : K), x^n) (λx, x^m) (𝓝 0) :=
+begin
+  let p := n - m,
+  have p_pos : 0 < p := nat.sub_pos_of_lt h,
+  have : n = m + p := (nat.add_sub_cancel' (le_of_lt h)).symm,
+  simp [this, pow_add],
+  have : (λ(x : K), x^m) = (λx, x^m * 1), by simp,
+  rw this,
+  apply is_o_mul_left (is_O_refl _ _) _,
+  rw is_o_iff_tendsto,
+  { simp only [div_one],
+    convert (continuous_pow p).tendsto (0 : K),
+    exact (zero_pow p_pos).symm },
+  { simp }
+end
+
+theorem is_o_pow_id {n : ℕ} (h : 1 < n) :
+  is_o (λ(x : K), x^n) (λx, x) (𝓝 0) :=
+by { convert is_o_pow_pow h, simp }
+
 end
 
 end asymptotics

src/analysis/calculus/deriv.lean

@@ -57,7 +57,7 @@ for Fréchet derivatives.
 
 universes u v w
 noncomputable theory
-open_locale classical
+open_locale classical topological_space
 open filter continuous_linear_map asymptotics set
 
 set_option class.instance_max_depth 100
@@ -87,7 +87,7 @@ has_deriv_at_filter f f' x (nhds_within x s)
 That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x`.
 -/
 def has_deriv_at (f : 𝕜 → F) (f' : F) (x : 𝕜) :=
-has_deriv_at_filter f f' x (nhds x)
+has_deriv_at_filter f f' x (𝓝 x)
 
 /--
 Derivative of `f` at the point `x` within the set `s`, if it exists.  Zero otherwise.
@@ -138,17 +138,21 @@ smul_right_one_eq_iff.mp $ unique_diff_within_at.eq H h h₁
 
 theorem has_deriv_at_filter_iff_tendsto :
   has_deriv_at_filter f f' x L ↔
-  tendsto (λ x' : 𝕜, ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) L (nhds 0) :=
+  tendsto (λ x' : 𝕜, ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) L (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
 theorem has_deriv_within_at_iff_tendsto : has_deriv_within_at f f' s x ↔
-  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (nhds_within x s) (nhds 0) :=
+  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (nhds_within x s) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
 theorem has_deriv_at_iff_tendsto : has_deriv_at f f' x ↔
-  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (nhds x) (nhds 0) :=
+  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝 x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
+theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔
+  is_o (λh, f (x + h) - f x - h • f') (λh, h) (𝓝 0) :=
+has_fderiv_at_iff_is_o_nhds_zero
+
 theorem has_deriv_at_filter.mono (h : has_deriv_at_filter f f' x L₂) (hst : L₁ ≤ L₂) :
   has_deriv_at_filter f f' x L₁ :=
 has_fderiv_at_filter.mono h hst
@@ -157,7 +161,7 @@ theorem has_deriv_within_at.mono (h : has_deriv_within_at f f' t x) (hst : s ⊆
   has_deriv_within_at f f' s x :=
 has_fderiv_within_at.mono h hst
 
-theorem has_deriv_at.has_deriv_at_filter (h : has_deriv_at f f' x) (hL : L ≤ nhds x) :
+theorem has_deriv_at.has_deriv_at_filter (h : has_deriv_at f f' x) (hL : L ≤ 𝓝 x) :
   has_deriv_at_filter f f' x L :=
 has_fderiv_at.has_fderiv_at_filter h hL
 
@@ -183,7 +187,7 @@ lemma has_deriv_within_at_inter' (h : t ∈ nhds_within x s) :
   has_deriv_within_at f f' (s ∩ t) x ↔ has_deriv_within_at f f' s x :=
 has_fderiv_within_at_inter' h
 
-lemma has_deriv_within_at_inter (h : t ∈ nhds x) :
+lemma has_deriv_within_at_inter (h : t ∈ 𝓝 x) :
   has_deriv_within_at f f' (s ∩ t) x ↔ has_deriv_within_at f f' s x :=
 has_fderiv_within_at_inter h
 
@@ -226,7 +230,7 @@ lemma deriv_within_subset (st : s ⊆ t) (ht : unique_diff_within_at 𝕜 s x)
 @[simp] lemma deriv_within_univ : deriv_within f univ = deriv f :=
 by { ext, unfold deriv_within deriv, rw fderiv_within_univ }
 
-lemma deriv_within_inter (ht : t ∈ nhds x) (hs : unique_diff_within_at 𝕜 s x) :
+lemma deriv_within_inter (ht : t ∈ 𝓝 x) (hs : unique_diff_within_at 𝕜 s x) :
   deriv_within f (s ∩ t) x = deriv_within f s x :=
 by { unfold deriv_within, rw fderiv_within_inter ht hs }
 
@@ -250,7 +254,7 @@ lemma has_deriv_within_at.congr_of_mem_nhds_within (h : has_deriv_within_at f f'
 has_deriv_at_filter.congr_of_mem_sets h h₁ hx
 
 lemma has_deriv_at.congr_of_mem_nhds (h : has_deriv_at f f' x)
-  (h₁ : {y | f₁ y = f y} ∈ nhds x) : has_deriv_at f₁ f' x :=
+  (h₁ : {y | f₁ y = f y} ∈ 𝓝 x) : has_deriv_at f₁ f' x :=
 has_deriv_at_filter.congr_of_mem_sets h h₁ (mem_of_nhds h₁ : _)
 
 lemma deriv_within_congr_of_mem_nhds_within (hs : unique_diff_within_at 𝕜 s x)
@@ -263,7 +267,7 @@ lemma deriv_within_congr (hs : unique_diff_within_at 𝕜 s x)
   deriv_within f₁ s x = deriv_within f s x :=
 by { unfold deriv_within, rw fderiv_within_congr hs hL hx }
 
-lemma deriv_congr_of_mem_nhds (hL : {y | f₁ y = f y} ∈ nhds x) : deriv f₁ x = deriv f x :=
+lemma deriv_congr_of_mem_nhds (hL : {y | f₁ y = f y} ∈ 𝓝 x) : deriv f₁ x = deriv f x :=
 by { unfold deriv, rwa fderiv_congr_of_mem_nhds }
 
 end congr
@@ -445,8 +449,8 @@ end sub
 section continuous
 
 theorem has_deriv_at_filter.tendsto_nhds
-  (hL : L ≤ nhds x) (h : has_deriv_at_filter f f' x L) :
-  tendsto f L (nhds (f x)) :=
+  (hL : L ≤ 𝓝 x) (h : has_deriv_at_filter f f' x L) :
+  tendsto f L (𝓝 (f x)) :=
 has_fderiv_at_filter.tendsto_nhds hL h
 
 theorem has_deriv_within_at.continuous_within_at

src/analysis/calculus/fderiv.lean

@@ -240,6 +240,31 @@ theorem has_fderiv_at_iff_tendsto : has_fderiv_at f f' x ↔
   tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) (𝓝 x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
+theorem has_fderiv_at_iff_is_o_nhds_zero : has_fderiv_at f f' x ↔
+  is_o (λh, f (x + h) - f x - f' h) (λh, h) (𝓝 0) :=
+begin
+  split,
+  { assume H,
+    have : 𝓝 0 ≤ comap (λ (z : E), z + x) (𝓝 (0 + x)),
+    { refine tendsto_iff_comap.mp _,
+      apply continuous.tendsto,
+      exact continuous_add continuous_id continuous_const },
+    apply is_o.mono this,
+    convert is_o.comp H (λz, z + x),
+    { ext h, simp },
+    { ext h, simp },
+    { simp } },
+  { assume H,
+    have : 𝓝 x ≤ comap (λ (z : E), z - x) (𝓝 (x - x)),
+    { refine tendsto_iff_comap.mp _,
+      apply continuous.tendsto,
+      exact continuous_add continuous_id continuous_const },
+    apply is_o.mono this,
+    convert is_o.comp H (λz, z - x),
+    { ext h, simp },
+    { simp } }
+end
+
 theorem has_fderiv_at_filter.mono (h : has_fderiv_at_filter f f' x L₂) (hst : L₁ ≤ L₂) :
   has_fderiv_at_filter f f' x L₁ :=
 is_o.mono hst h