feat(analysis/complex/exponential): derivatives (#1695)

* feat(analysis/complex/exponential): derivatives

* nhds

* nhds

* remove omega

* remove set_option

* simp attributes, field type

* restrict scalar

* staging

* complete proof

* staging

* cleanup

* staging

* cleanup

* docstring

* docstring

* reviewer's comments

* real derivatives of exp, sin, cos, sinh, cosh

* fix build

* remove priority

* better proofs

Author: sgouezel

src/analysis/asymptotics.lean

@@ -42,14 +42,22 @@ open_locale topological_space
 
 namespace asymptotics
 
-variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
+variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {𝕜 : Type*} {𝕜' : Type*}
 
 section
 variables [has_norm β] [has_norm γ] [has_norm δ]
 
+/-- The Landau notation `is_O f g l` where `f` and `g` are two functions on a type `α` and `l` is
+a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by a constant multiple of `∥g∥`.
+In other words, `∥f∥ / ∥g∥` is eventually bounded, modulo division by zero issues that are avoided
+by this definition. -/
 def is_O (f : α → β) (g : α → γ) (l : filter α) : Prop :=
 ∃ c > 0, { x | ∥ f x ∥ ≤ c * ∥ g x ∥ } ∈ l
 
+/-- The Landau notation `is_o f g l` where `f` and `g` are two functions on a type `α` and `l` is
+a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by an arbitrarily small constant
+multiple of `∥g∥`. In other words, `∥f∥ / ∥g∥` tends to `0` along `l`, modulo division by zero
+issues that are avoided by this definition. -/
 def is_o (f : α → β) (g : α → γ) (l : filter α) : Prop :=
 ∀ c > 0, { x | ∥ f x ∥ ≤  c * ∥ g x ∥ } ∈ l
 
@@ -450,12 +458,12 @@ end
 end
 
 section
-variables [has_norm β] [normed_field γ]
+variables [has_norm β] [normed_field 𝕜]
 
 open normed_field
 
 theorem is_O_const_one (c : β) (l : filter α) :
-  is_O (λ x : α, c) (λ x, (1 : γ)) l :=
+  is_O (λ x : α, c) (λ x, (1 : 𝕜)) l :=
 begin
   rw is_O_iff,
   refine ⟨∥c∥, _⟩,
@@ -467,9 +475,9 @@ end
 end
 
 section
-variables [normed_field β] [normed_group γ]
+variables [normed_field 𝕜] [normed_group γ]
 
-theorem is_O_const_mul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) (c : β) :
+theorem is_O_const_mul_left {f : α → 𝕜} {g : α → γ} {l : filter α} (h : is_O f g l) (c : 𝕜) :
   is_O (λ x, c * f x) g l :=
  begin
   cases classical.em (c = 0) with h'' h'',
@@ -484,7 +492,7 @@ theorem is_O_const_mul_left {f : α → β} {g : α → γ} {l : filter α} (h :
   exact mul_le_mul_of_nonneg_left h₀ (norm_nonneg _)
 end
 
-theorem is_O_const_mul_left_iff {f : α → β} {g : α → γ} {l : filter α} {c : β} (hc : c ≠ 0) :
+theorem is_O_const_mul_left_iff {f : α → 𝕜} {g : α → γ} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_O (λ x, c * f x) g l ↔ is_O f g l :=
 begin
   split,
@@ -494,8 +502,7 @@ begin
   intro h, apply is_O_const_mul_left h
 end
 
-theorem is_o_const_mul_left {f : α → β} {g : α → γ} {l : filter α}
-    (h : is_o f g l) (c : β) :
+theorem is_o_const_mul_left {f : α → 𝕜} {g : α → γ} {l : filter α} (h : is_o f g l) (c : 𝕜) :
   is_o (λ x, c * f x) g l :=
 begin
   cases classical.em (c = 0) with h'' h'',
@@ -509,7 +516,7 @@ begin
   rw [←mul_assoc, mul_div_cancel' _ cne0]
 end
 
-theorem is_o_const_mul_left_iff {f : α → β} {g : α → γ} {l : filter α} {c : β} (hc : c ≠ 0) :
+theorem is_o_const_mul_left_iff {f : α → 𝕜} {g : α → γ} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_o (λ x, c * f x) g l ↔ is_o f g l :=
 begin
   split,
@@ -523,9 +530,9 @@ end
 end
 
 section
-variables [normed_group β] [normed_field γ]
+variables [normed_group β] [normed_field 𝕜]
 
-theorem is_O_of_is_O_const_mul_right {f : α → β} {g : α → γ} {l : filter α} {c : γ}
+theorem is_O_of_is_O_const_mul_right {f : α → β} {g : α → 𝕜} {l : filter α} {c : 𝕜}
     (h : is_O f (λ x, c * g x) l) :
   is_O f g l  :=
 begin
@@ -539,7 +546,7 @@ begin
   rw [normed_field.norm_mul, mul_assoc]
 end
 
-theorem is_O_const_mul_right_iff {f : α → β} {g : α → γ} {l : filter α} {c : γ} (hc : c ≠ 0) :
+theorem is_O_const_mul_right_iff {f : α → β} {g : α → 𝕜} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_O f (λ x, c * g x) l ↔ is_O f g l :=
 begin
   split,
@@ -550,7 +557,7 @@ begin
   convert h, ext, rw [←mul_assoc, inv_mul_cancel hc, one_mul]
 end
 
-theorem is_o_of_is_o_const_mul_right {f : α → β} {g : α → γ} {l : filter α} {c : γ}
+theorem is_o_of_is_o_const_mul_right {f : α → β} {g : α → 𝕜} {l : filter α} {c : 𝕜}
     (h : is_o f (λ x, c * g x) l) :
   is_o f g l  :=
 begin
@@ -563,7 +570,7 @@ begin
   ext x, rw [normed_field.norm_mul, ←mul_assoc, div_mul_cancel _ cne0]
 end
 
-theorem is_o_const_mul_right {f : α → β} {g : α → γ} {l : filter α} {c : γ} (hc : c ≠ 0) :
+theorem is_o_const_mul_right {f : α → β} {g : α → 𝕜} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_o f (λ x, c * g x) l ↔ is_o f g l :=
 begin
   split,
@@ -575,7 +582,7 @@ begin
 end
 
 theorem is_o_one_iff {f : α → β} {l : filter α} :
-  is_o f (λ x, (1 : γ)) l ↔ tendsto f l (𝓝 0) :=
+  is_o f (λ x, (1 : 𝕜)) l ↔ tendsto f l (𝓝 0) :=
 begin
   rw [normed_group.tendsto_nhds_zero, is_o], split,
   { intros h e epos,
@@ -589,7 +596,7 @@ begin
 end
 
 theorem is_O_one_of_tendsto {f : α → β} {l : filter α} {y : β}
-  (h : tendsto f l (𝓝 y)) : is_O f (λ x, (1 : γ)) l :=
+  (h : tendsto f l (𝓝 y)) : is_O f (λ x, (1 : 𝕜)) l :=
 begin
   have Iy : ∥y∥ < ∥y∥ + 1 := lt_add_one _,
   refine ⟨∥y∥ + 1, lt_of_le_of_lt (norm_nonneg _) Iy, _⟩,
@@ -616,9 +623,9 @@ h₁.to_is_O.trans_tendsto
 end
 
 section
-variables [normed_field β] [normed_field γ]
+variables [normed_field 𝕜] [normed_field 𝕜']
 
-theorem is_O_mul {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
+theorem is_O_mul {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} {l : filter α}
     (h₁ : is_O f₁ g₁ l) (h₂ : is_O f₂ g₂ l) :
   is_O (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
 begin
@@ -631,7 +638,7 @@ begin
   exact mul_le_mul hx₁ hx₂ (norm_nonneg _) (mul_nonneg (le_of_lt c₁pos) (norm_nonneg _))
 end
 
-theorem is_o_mul_left {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
+theorem is_o_mul_left {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} {l : filter α}
     (h₁ : is_O f₁ g₁ l) (h₂ : is_o f₂ g₂ l) :
   is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
 begin
@@ -645,12 +652,12 @@ begin
   rw [mul_left_comm]
 end
 
-theorem is_o_mul_right {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
+theorem is_o_mul_right {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} {l : filter α}
     (h₁ : is_o f₁ g₁ l) (h₂ : is_O f₂ g₂ l) :
   is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
 by convert is_o_mul_left h₂ h₁; simp only [mul_comm]
 
-theorem is_o_mul {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
+theorem is_o_mul {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} {l : filter α}
     (h₁ : is_o f₁ g₁ l) (h₂ : is_o f₂ g₂ l) :
   is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
 is_o_mul_left h₁.to_is_O h₂
@@ -663,11 +670,11 @@ scalar multiplication is multiplication.
 -/
 
 section
-variables {K : Type*} [normed_field K] [normed_group β] [normed_space K β] [normed_group γ]
+variables [normed_field 𝕜] [normed_group β] [normed_space 𝕜 β] [normed_group γ]
 
 set_option class.instance_max_depth 43
 
-theorem is_O_const_smul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) (c : K) :
+theorem is_O_const_smul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) (c : 𝕜) :
   is_O (λ x, c • f x) g l :=
 begin
   rw [←is_O_norm_left], simp only [norm_smul],
@@ -676,15 +683,15 @@ begin
   apply h
 end
 
-theorem is_O_const_smul_left_iff {f : α → β} {g : α → γ} {l : filter α} {c : K} (hc : c ≠ 0) :
+theorem is_O_const_smul_left_iff {f : α → β} {g : α → γ} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_O (λ x, c • f x) g l ↔ is_O f g l :=
 begin
   have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
   rw [←is_O_norm_left], simp only [norm_smul],
   rw [is_O_const_mul_left_iff cne0, is_O_norm_left]
 end
 
-theorem is_o_const_smul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_o f g l) (c : K) :
+theorem is_o_const_smul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_o f g l) (c : 𝕜) :
   is_o (λ x, c • f x) g l :=
 begin
   rw [←is_o_norm_left], simp only [norm_smul],
@@ -693,7 +700,7 @@ begin
   apply h
 end
 
-theorem is_o_const_smul_left_iff {f : α → β} {g : α → γ} {l : filter α} {c : K} (hc : c ≠ 0) :
+theorem is_o_const_smul_left_iff {f : α → β} {g : α → γ} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_o (λ x, c • f x) g l ↔ is_o f g l :=
 begin
   have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
@@ -704,19 +711,19 @@ end
 end
 
 section
-variables {K : Type*} [normed_group β] [normed_field K] [normed_group γ] [normed_space K γ]
+variables [normed_group β] [normed_field 𝕜] [normed_group γ] [normed_space 𝕜 γ]
 
 set_option class.instance_max_depth 43
 
-theorem is_O_const_smul_right {f : α → β} {g : α → γ} {l : filter α} {c : K} (hc : c ≠ 0) :
+theorem is_O_const_smul_right {f : α → β} {g : α → γ} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_O f (λ x, c • g x) l ↔ is_O f g l :=
 begin
   have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
   rw [←is_O_norm_right], simp only [norm_smul],
   rw [is_O_const_mul_right_iff cne0, is_O_norm_right]
 end
 
-theorem is_o_const_smul_right {f : α → β} {g : α → γ} {l : filter α} {c : K} (hc : c ≠ 0) :
+theorem is_o_const_smul_right {f : α → β} {g : α → γ} {l : filter α} {c : 𝕜} (hc : c ≠ 0) :
   is_o f (λ x, c • g x) l ↔ is_o f g l :=
 begin
   have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
@@ -727,12 +734,12 @@ end
 end
 
 section
-variables {K : Type*} [normed_field K] [normed_group β] [normed_space K β]
-[normed_group γ] [normed_space K γ]
+variables [normed_field 𝕜] [normed_group β] [normed_space 𝕜 β]
+[normed_group γ] [normed_space 𝕜 γ]
 
 set_option class.instance_max_depth 43
 
-theorem is_O_smul {k : α → K} {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) :
+theorem is_O_smul {k : α → 𝕜} {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) :
   is_O (λ x, k x • f x) (λ x, k x • g x) l :=
 begin
   rw [←is_O_norm_left, ←is_O_norm_right], simp only [norm_smul],
@@ -741,7 +748,7 @@ begin
   exact h
 end
 
-theorem is_o_smul {k : α → K} {f : α → β} {g : α → γ} {l : filter α} (h : is_o f g l) :
+theorem is_o_smul {k : α → 𝕜} {f : α → β} {g : α → γ} {l : filter α} (h : is_o f g l) :
   is_o (λ x, k x • f x) (λ x, k x • g x) l :=
 begin
   rw [←is_o_norm_left, ←is_o_norm_right], simp only [norm_smul],
@@ -753,13 +760,13 @@ end
 end
 
 section
-variables [normed_field β]
+variables [normed_field 𝕜]
 
-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 : α → 𝕜} {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 : 𝕜)) l,
   begin
     use [1, zero_lt_one],
     filter_upwards [univ_mem_sets], simp,
@@ -769,10 +776,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 : α → 𝕜} {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 : 𝕜)) 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,
@@ -787,11 +794,27 @@ 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 : α → 𝕜} {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 : 𝕜), x^n) (λx, x^m) (𝓝 0) :=
+begin
+  let p := n - m,
+  have nmp : n = m + p := (nat.add_sub_cancel' (le_of_lt h)).symm,
+  have : (λ(x : 𝕜), x^m) = (λx, x^m * 1), by simp,
+  simp only [this, pow_add, nmp],
+  refine is_o_mul_left (is_O_refl _ _) (is_o_one_iff.2 _),
+  convert (continuous_pow p).tendsto (0 : 𝕜),
+  exact (zero_pow (nat.sub_pos_of_lt h)).symm
+end
+
+theorem is_o_pow_id {n : ℕ} (h : 1 < n) :
+  is_o (λ(x : 𝕜), x^n) (λx, x) (𝓝 0) :=
+by { convert is_o_pow_pow h, simp }
+
 end
 
 end asymptotics