From 8bf24777564e29dc7c30170f49f810dde95ac147 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 19 Oct 2022 09:54:19 +0000
Subject: [PATCH] feat(analysis/asymptotics): prove that a function has
 derivative 0 using asymptotics (#16934)

* From the sphere eversion project
* Needed for computing derivatives of the parametric interval integral

Co-authored by: Patrick Massot [patrickmassot@free.fr](patrickmassot@free.fr)
---
 src/analysis/asymptotics/asymptotics.lean | 33 +++++++++++++++++++++++
 src/analysis/calculus/fderiv.lean         | 32 +++++++++++++++++++---
 src/analysis/normed/field/basic.lean      |  2 ++
 3 files changed, 64 insertions(+), 3 deletions(-)

diff --git a/src/analysis/asymptotics/asymptotics.lean b/src/analysis/asymptotics/asymptotics.lean
index 970336579d7cd..3543859939d16 100644
--- a/src/analysis/asymptotics/asymptotics.lean
+++ b/src/analysis/asymptotics/asymptotics.lean
@@ -101,6 +101,9 @@ by simp only [is_O, is_O_with]
 lemma is_O.of_bound (c : ℝ) (h : ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥) : f =O[l] g :=
 is_O_iff.2 ⟨c, h⟩
 
+lemma is_O.of_bound' (h : ∀ᶠ x in l, ∥f x∥ ≤ ∥g x∥) : f =O[l] g :=
+is_O.of_bound 1 $ by { simp_rw one_mul, exact h }
+
 lemma is_O.bound : f =O[l] g → ∃ c : ℝ, ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥ := is_O_iff.1
 
 /-- The Landau notation `f =o[l] g` where `f` and `g` are two functions on a type `α` and `l` is
@@ -382,6 +385,14 @@ let ⟨c, cpos, hc⟩ := hfg.exists_pos in hc.trans_is_o hgk cpos
   (hgk : g =o[l] k) : f =o[l] k :=
 hfg.trans_is_O_with hgk.is_O_with one_pos
 
+lemma _root_.filter.eventually.trans_is_O {f : α → E} {g : α → F'} {k : α → G}
+  (hfg : ∀ᶠ x in l, ∥f x∥ ≤ ∥g x∥) (hgk : g =O[l] k) : f =O[l] k :=
+(is_O.of_bound' hfg).trans hgk
+
+lemma _root_.filter.eventually.is_O {f : α → E} {g : α → ℝ} {l : filter α}
+  (hfg : ∀ᶠ x in l, ∥f x∥ ≤ g x) : f =O[l] g :=
+is_O.of_bound' $ hfg.mono $ λ x hx, hx.trans $ real.le_norm_self _
+
 section
 
 variable (l)
@@ -1547,6 +1558,28 @@ theorem is_o_norm_pow_id {n : ℕ} (h : 1 < n) :
   (λ x : E', ∥x∥^n) =o[𝓝 0] (λ x, x) :=
 by simpa only [pow_one, is_o_norm_right] using @is_o_norm_pow_norm_pow E' _ _ _ h
 
+lemma is_O.eq_zero_of_norm_pow_within {f : E'' → F''} {s : set E''} {x₀ : E''} {n : ℕ}
+  (h : f =O[𝓝[s] x₀] λ x, ∥x - x₀∥ ^ n) (hx₀ : x₀ ∈ s) (hn : 0 < n) : f x₀ = 0 :=
+mem_of_mem_nhds_within hx₀ h.eq_zero_imp $ by simp_rw [sub_self, norm_zero, zero_pow hn]
+
+lemma is_O.eq_zero_of_norm_pow {f : E'' → F''} {x₀ : E''} {n : ℕ}
+  (h : f =O[𝓝 x₀] λ x, ∥x - x₀∥ ^ n) (hn : 0 < n) : f x₀ = 0 :=
+by { rw [← nhds_within_univ] at h, exact h.eq_zero_of_norm_pow_within (mem_univ _) hn }
+
+lemma is_o_pow_sub_pow_sub (x₀ : E') {n m : ℕ} (h : n < m) :
+    (λ x, ∥x - x₀∥ ^ m) =o[𝓝 x₀] λ x, ∥x - x₀∥^n :=
+begin
+  have : tendsto (λ x, ∥x - x₀∥) (𝓝 x₀) (𝓝 0),
+  { apply tendsto_norm_zero.comp,
+    rw ← sub_self x₀,
+    exact tendsto_id.sub tendsto_const_nhds },
+  exact (is_o_pow_pow h).comp_tendsto this
+end
+
+lemma is_o_pow_sub_sub (x₀ : E') {m : ℕ} (h : 1 < m) :
+    (λ x, ∥x - x₀∥^m) =o[𝓝 x₀] λ x, x - x₀ :=
+by simpa only [is_o_norm_right, pow_one] using is_o_pow_sub_pow_sub x₀ h
+
 theorem is_O_with.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c l f₁ f₂) (hc : c < 1) :
   is_O_with (1 / (1 - c)) l f₂ (λx, f₂ x - f₁ x) :=
 is_O_with.of_bound $ mem_of_superset h.bound $ λ x hx,
diff --git a/src/analysis/calculus/fderiv.lean b/src/analysis/calculus/fderiv.lean
index 4b4525da1bebc..90fa617b7b12f 100644
--- a/src/analysis/calculus/fderiv.lean
+++ b/src/analysis/calculus/fderiv.lean
@@ -346,6 +346,8 @@ lemma has_fderiv_at.differentiable_at (h : has_fderiv_at f f' x) : differentiabl
   has_fderiv_within_at f f' univ x ↔ has_fderiv_at f f' x :=
 by { simp only [has_fderiv_within_at, nhds_within_univ], refl }
 
+alias has_fderiv_within_at_univ ↔ has_fderiv_within_at.has_fderiv_at_of_univ _
+
 lemma has_fderiv_within_at_insert {y : E} {g' : E →L[𝕜] F}  :
   has_fderiv_within_at g g' (insert y s) x ↔ has_fderiv_within_at g g' s x :=
 begin
@@ -406,7 +408,7 @@ lemma has_fderiv_at.lim (hf : has_fderiv_at f f' x) (v : E) {α : Type*} {c : α
   {l : filter α} (hc : tendsto (λ n, ∥c n∥) l at_top) :
   tendsto (λ n, (c n) • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 (f' v)) :=
 begin
-  refine (has_fderiv_within_at_univ.2 hf).lim _ (univ_mem' (λ _, trivial)) hc _,
+  refine (has_fderiv_within_at_univ.2 hf).lim _ univ_mem hc _,
   assume U hU,
   refine (eventually_ne_of_tendsto_norm_at_top hc (0:𝕜)).mono (λ y hy, _),
   convert mem_of_mem_nhds hU,
@@ -646,6 +648,30 @@ lemma fderiv_within_mem_iff {f : E → F} {t : set E} {s : set (E →L[𝕜] F)}
 by by_cases hx : differentiable_within_at 𝕜 f t x;
   simp [fderiv_within_zero_of_not_differentiable_within_at, *]
 
+lemma asymptotics.is_O.has_fderiv_within_at {s : set E} {x₀ : E} {n : ℕ}
+  (h : f =O[𝓝[s] x₀] λ x, ∥x - x₀∥^n) (hx₀ : x₀ ∈ s) (hn : 1 < n) :
+  has_fderiv_within_at f (0 : E →L[𝕜] F) s x₀ :=
+by simp_rw [has_fderiv_within_at, has_fderiv_at_filter,
+  h.eq_zero_of_norm_pow_within hx₀ $ zero_lt_one.trans hn, zero_apply, sub_zero,
+  h.trans_is_o ((is_o_pow_sub_sub x₀ hn).mono nhds_within_le_nhds)]
+
+lemma asymptotics.is_O.has_fderiv_at {x₀ : E} {n : ℕ}
+  (h : f =O[𝓝 x₀] λ x, ∥x - x₀∥^n) (hn : 1 < n) :
+  has_fderiv_at f (0 : E →L[𝕜] F) x₀ :=
+begin
+  rw [← nhds_within_univ] at h,
+  exact (h.has_fderiv_within_at (mem_univ _) hn).has_fderiv_at_of_univ
+end
+
+lemma has_fderiv_within_at.is_O {f : E → F} {s : set E} {x₀ : E} {f' : E →L[𝕜] F}
+  (h : has_fderiv_within_at f f' s x₀) :
+  (λ x, f x - f x₀) =O[𝓝[s] x₀] λ x, x - x₀ :=
+by simpa only [sub_add_cancel] using h.is_O.add (is_O_sub f' (𝓝[s] x₀) x₀)
+
+lemma has_fderiv_at.is_O {f : E → F} {x₀ : E} {f' : E →L[𝕜] F} (h : has_fderiv_at f f' x₀) :
+  (λ x, f x - f x₀) =O[𝓝 x₀] λ x, x - x₀ :=
+by simpa only [sub_add_cancel] using h.is_O.add (is_O_sub f' (𝓝 x₀) x₀)
+
 end fderiv_properties
 
 section continuous
@@ -2699,7 +2725,7 @@ end
 
 lemma comp_has_fderiv_at_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
   has_fderiv_at (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ has_fderiv_at f f' x :=
-by rw [← has_fderiv_within_at_univ, ← has_fderiv_within_at_univ, iso.comp_has_fderiv_within_at_iff]
+by simp_rw [← has_fderiv_within_at_univ, iso.comp_has_fderiv_within_at_iff]
 
 lemma comp_has_fderiv_within_at_iff'
   {f : G → E} {s : set G} {x : G} {f' : G →L[𝕜] F} :
@@ -2710,7 +2736,7 @@ by rw [← iso.comp_has_fderiv_within_at_iff, ← continuous_linear_map.comp_ass
 
 lemma comp_has_fderiv_at_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
   has_fderiv_at (iso ∘ f) f' x ↔ has_fderiv_at f ((iso.symm : F →L[𝕜] E).comp f') x :=
-by rw [← has_fderiv_within_at_univ, ← has_fderiv_within_at_univ, iso.comp_has_fderiv_within_at_iff']
+by simp_rw [← has_fderiv_within_at_univ, iso.comp_has_fderiv_within_at_iff']
 
 lemma comp_fderiv_within {f : G → E} {s : set G} {x : G}
   (hxs : unique_diff_within_at 𝕜 s x) :
diff --git a/src/analysis/normed/field/basic.lean b/src/analysis/normed/field/basic.lean
index fd035c2cbe88e..7920b8e0fb064 100644
--- a/src/analysis/normed/field/basic.lean
+++ b/src/analysis/normed/field/basic.lean
@@ -638,6 +638,8 @@ abs_of_nonneg hx
 lemma norm_of_nonpos {x : ℝ} (hx : x ≤ 0) : ∥x∥ = -x :=
 abs_of_nonpos hx
 
+lemma le_norm_self (r : ℝ) : r ≤ ∥r∥ := le_abs_self r
+
 @[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
 
 @[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥(n : ℝ)∥₊ = n := nnreal.eq $ by simp