refactor(analysis/asymptotics): make is_o irreducible (leanprover-community#2416)

`is_o` is currently not irreducible. Since it is a complicated type, Lean can have trouble checking if two types with `is_o` are defeq or not, leading to timeouts as described in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/undergraduate.20calculus/near/193776607
This PR makes `is_o` irreducible.

Author: sgouezel

src/analysis/asymptotics.lean

@@ -66,18 +66,53 @@ avoided by this definition. Probably you want to use `is_O` instead of this rela
 def is_O_with (c : ℝ) (f : α → E) (g : α → F) (l : filter α) : Prop :=
 ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥
 
+/-- Definition of `is_O_with`. We record it in a lemma as we will set `is_O_with` to be irreducible
+at the end of this file. -/
+lemma is_O_with_iff {c : ℝ} {f : α → E} {g : α → F} {l : filter α} :
+  is_O_with c f g l ↔ ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥ := iff.rfl
+
+lemma is_O_with.of_bound {c : ℝ} {f : α → E} {g : α → F} {l : filter α}
+  (h : ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥) : is_O_with c f g l := h
+
 /-- 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 : α → E) (g : α → F) (l : filter α) : Prop := ∃ c : ℝ, is_O_with c f g l
 
+/-- Definition of `is_O` in terms of `is_O_with`. We record it in a lemma as we will set
+`is_O` to be irreducible at the end of this file. -/
+lemma is_O_iff_is_O_with {f : α → E} {g : α → F} {l : filter α} :
+  is_O f g l ↔ ∃ c : ℝ, is_O_with c f g l := iff.rfl
+
+/-- Definition of `is_O` in terms of filters. We record it in a lemma as we will set
+`is_O` to be irreducible at the end of this file. -/
+lemma is_O_iff {f : α → E} {g : α → F} {l : filter α} :
+  is_O f g l ↔ ∃ c : ℝ, ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥ := iff.rfl
+
+lemma is_O.of_bound (c : ℝ) {f : α → E} {g : α → F} {l : filter α}
+  (h : ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥) : is_O f g l := ⟨c, h⟩
+
 /-- 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 : α → E) (g : α → F) (l : filter α) : Prop := ∀ ⦃c : ℝ⦄, 0 < c → is_O_with c f g l
 
+/-- Definition of `is_o` in terms of `is_O_with`. We record it in a lemma as we will set
+`is_o` to be irreducible at the end of this file. -/
+lemma is_o_iff_forall_is_O_with {f : α → E} {g : α → F} {l : filter α} :
+  is_o f g l ↔ ∀ ⦃c : ℝ⦄, 0 < c → is_O_with c f g l := iff.rfl
+
+/-- Definition of `is_o` in terms of filters. We record it in a lemma as we will set
+`is_o` to be irreducible at the end of this file. -/
+lemma is_o_iff {f : α → E} {g : α → F} {l : filter α} :
+  is_o f g l ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥ := iff.rfl
+
+lemma is_o.def {f : α → E} {g : α → F} {l : filter α} (h : is_o f g l) {c : ℝ} (hc : 0 < c) :
+  ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥ :=
+h hc
+
 end defs
 
 /-! ### Conversions -/
@@ -1058,3 +1093,5 @@ lemma is_o_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
 forall_congr $ λ c, forall_congr $ λ hc, e.is_O_with_congr
 
 end homeomorph
+
+attribute [irreducible] asymptotics.is_o asymptotics.is_O asymptotics.is_O_with

src/analysis/calculus/extend_deriv.lean

@@ -46,6 +46,7 @@ begin
   by_cases hx : x ∉ closure s,
   { rw ← closure_closure at hx, exact has_fderiv_within_at_of_not_mem_closure hx },
   push_neg at hx,
+  rw [has_fderiv_within_at, has_fderiv_at_filter, asymptotics.is_o_iff],
   /- One needs to show that `∥f y - f x∥ ≤ ε ∥y - x∥` for `y` close to `x` in `closure s`, where
   `ε` is an arbitrary positive constant. By continuity of the functions, it suffices to prove this
   for nearby points inside `s`. In a neighborhood of `x`, the derivative of `f` is arbitrarily small

src/analysis/calculus/fderiv.lean

@@ -319,7 +319,10 @@ h.is_O.congr_of_sub.2 (f'.is_O_sub _ _)
 
 lemma has_strict_fderiv_at.has_fderiv_at (hf : has_strict_fderiv_at f f' x) :
   has_fderiv_at f f' x :=
-λ c hc, tendsto_id.prod_mk_nhds tendsto_const_nhds (hf hc)
+begin
+  rw [has_fderiv_at, has_fderiv_at_filter, is_o_iff],
+  exact (λ c hc, tendsto_id.prod_mk_nhds tendsto_const_nhds (is_o_iff.1 hf hc))
+end
 
 lemma has_strict_fderiv_at.differentiable_at (hf : has_strict_fderiv_at f f' x) :
   differentiable_at 𝕜 f x :=
@@ -1615,7 +1618,7 @@ begin
   apply is_bounded_bilinear_map_apply.is_O_comp.trans_is_o,
   refine is_o.trans_is_O _ (is_O_const_mul_self 1 _ _).of_norm_right,
   refine is_o.mul_is_O _ (is_O_refl _ _),
-  exact (((h.is_bounded_linear_map_deriv.is_O_id ⊤).comp_tendsto le_top).trans_is_o this).norm_left
+  exact (((h.is_bounded_linear_map_deriv.is_O_id ⊤).comp_tendsto le_top : _).trans_is_o this).norm_left
 end
 
 lemma is_bounded_bilinear_map.has_fderiv_at (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :

src/analysis/complex/exponential.lean

@@ -49,7 +49,7 @@ lemma has_deriv_at_exp (x : ℂ) : has_deriv_at exp (exp x) x :=
 begin
   rw has_deriv_at_iff_is_o_nhds_zero,
   have : (1 : ℕ) < 2 := by norm_num,
-  refine is_O.trans_is_o ⟨∥exp x∥, _⟩ (is_o_pow_id this),
+  refine (is_O.of_bound (∥exp x∥) _).trans_is_o (is_o_pow_id this),
   have : metric.ball (0 : ℂ) 1 ∈ nhds (0 : ℂ) := metric.ball_mem_nhds 0 zero_lt_one,
   apply filter.mem_sets_of_superset this (λz hz, _),
   simp only [metric.mem_ball, dist_zero_right] at hz,

src/analysis/normed_space/bounded_linear_maps.lean

@@ -128,8 +128,7 @@ open asymptotics filter
 
 theorem is_O_id {f : E → F} (h : is_bounded_linear_map 𝕜 f) (l : filter E) :
   is_O f (λ x, x) l :=
-let ⟨M, hMp, hM⟩ := h.bound in
-⟨M, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
+let ⟨M, hMp, hM⟩ := h.bound in is_O.of_bound _ (mem_sets_of_superset univ_mem_sets (λ x _, hM x))
 
 theorem is_O_comp {E : Type*} {g : F → G} (hg : is_bounded_linear_map 𝕜 g)
   {f : E → F} (l : filter E) : is_O (λ x', g (f x')) f l :=
@@ -222,8 +221,8 @@ variable {f : E × F → G}
 
 protected lemma is_bounded_bilinear_map.is_O (h : is_bounded_bilinear_map 𝕜 f) :
   asymptotics.is_O f (λ p : E × F, ∥p.1∥ * ∥p.2∥) ⊤ :=
-let ⟨C, Cpos, hC⟩ := h.bound in
-⟨C, filter.eventually_of_forall ⊤ $ λ ⟨x, y⟩, by simpa [mul_assoc] using hC x y⟩
+let ⟨C, Cpos, hC⟩ := h.bound in asymptotics.is_O.of_bound _ $
+filter.eventually_of_forall ⊤ $ λ ⟨x, y⟩, by simpa [mul_assoc] using hC x y
 
 lemma is_bounded_bilinear_map.is_O_comp {α : Type*} (H : is_bounded_bilinear_map 𝕜 f)
   {g : α → E} {h : α → F} {l : filter α} :