feat(analysis/asymptotics/asymptotics): generalize, golf (#15010)

* add `is_o_iff_nat_mul_le`, `is_o_iff_nat_mul_le'`, `is_o_irrefl`, `is_O.not_is_o`, `is_o.not_is_O`;
* generalize lemmas about `1 = o(f)`, `1 = O(f)`, `f = o(1)`, `f = O(1)` to `[has_one F] [norm_one_class F]`, add some `@[simp]` attrs;
* rename `is_O_one_of_tendsto` to `filter.tendsto.is_O_one`;
* golf some proofs

src/analysis/analytic/basic.lean

@@ -222,7 +222,7 @@ in ⟨⟨C, hC.lt.le⟩, hC, by exact_mod_cast hp⟩
 
 lemma le_radius_of_tendsto (p : formal_multilinear_series 𝕜 E F) {l : ℝ}
   (h : tendsto (λ n, ∥p n∥ * r^n) at_top (𝓝 l)) : ↑r ≤ p.radius :=
-p.le_radius_of_is_O (is_O_one_of_tendsto _ h)
+p.le_radius_of_is_O (h.is_O_one _)
 
 lemma le_radius_of_summable_norm (p : formal_multilinear_series 𝕜 E F)
   (hs : summable (λ n, ∥p n∥ * r^n)) : ↑r ≤ p.radius :=

src/analysis/asymptotics/asymptotics.lean

@@ -178,6 +178,36 @@ lemma is_O.exists_mem_basis {ι} {p : ι → Prop} {s : ι → set α} (h : f =O
 flip Exists₂.imp h.exists_pos $ λ c hc h,
   by simpa only [is_O_with_iff, hb.eventually_iff, exists_prop] using h
 
+lemma is_O_with_inv (hc : 0 < c) : is_O_with c⁻¹ l f g ↔ ∀ᶠ x in l, c * ∥f x∥ ≤ ∥g x∥ :=
+by simp only [is_O_with, ← div_eq_inv_mul, le_div_iff' hc]
+
+-- We prove this lemma with strange assumptions to get two lemmas below automatically
+lemma is_o_iff_nat_mul_le_aux (h₀ : (∀ x, 0 ≤ ∥f x∥) ∨ ∀ x, 0 ≤ ∥g x∥) :
+  f =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ∥f x∥ ≤ ∥g x∥ :=
+begin
+  split,
+  { rintro H (_|n),
+    { refine (H.def one_pos).mono (λ x h₀', _),
+      rw [nat.cast_zero, zero_mul],
+      refine h₀.elim (λ hf, (hf x).trans _) (λ hg, hg x),
+      rwa one_mul at h₀' },
+    { have : (0 : ℝ) < n.succ, from nat.cast_pos.2 n.succ_pos,
+      exact (is_O_with_inv this).1 (H.def' $ inv_pos.2 this) } },
+  { refine λ H, is_o_iff.2 (λ ε ε0, _),
+    rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩,
+    have hn₀ : (0 : ℝ) < n, from (inv_pos.2 ε0).trans hn,
+    refine ((is_O_with_inv hn₀).2 (H n)).bound.mono (λ x hfg, _),
+    refine hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le ε0 hn.le) _),
+    refine h₀.elim (λ hf, nonneg_of_mul_nonneg_right ((hf x).trans hfg) _) (λ h, h x),
+    exact inv_pos.2 hn₀ }
+end
+
+lemma is_o_iff_nat_mul_le : f =o[l] g' ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ∥f x∥ ≤ ∥g' x∥ :=
+is_o_iff_nat_mul_le_aux (or.inr $ λ x, norm_nonneg _)
+
+lemma is_o_iff_nat_mul_le' : f' =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ∥f' x∥ ≤ ∥g x∥ :=
+is_o_iff_nat_mul_le_aux (or.inl $ λ x, norm_nonneg _)
+
 /-! ### Subsingleton -/
 
 @[nontriviality] lemma is_o_of_subsingleton [subsingleton E'] : f' =o[l] g' :=
@@ -385,6 +415,23 @@ hfg.trans (is_O_of_le l hgk)
 theorem is_o.trans_le (hfg : f =o[l] g) (hgk : ∀ x, ∥g x∥ ≤ ∥k x∥) : f =o[l] k :=
 hfg.trans_is_O_with (is_O_with_of_le _ hgk) zero_lt_one
 
+theorem is_o_irrefl' (h : ∃ᶠ x in l, ∥f' x∥ ≠ 0) : ¬f' =o[l] f' :=
+begin
+  intro ho,
+  rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩,
+  rw [one_div, ← div_eq_inv_mul] at hle,
+  exact (half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_le hle
+end
+
+theorem is_o_irrefl (h : ∃ᶠ x in l, f'' x ≠ 0) : ¬f'' =o[l] f'' :=
+is_o_irrefl' $ h.mono $ λ x, norm_ne_zero_iff.mpr
+
+theorem is_O.not_is_o (h : f'' =O[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) : ¬g' =o[l] f'' :=
+λ h', is_o_irrefl hf (h.trans_is_o h')
+
+theorem is_o.not_is_O (h : f'' =o[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) : ¬g' =O[l] f'' :=
+λ h', is_o_irrefl hf (h.trans_is_O h')
+
 section bot
 
 variables (c f g)
@@ -830,47 +877,56 @@ by rw is_O_iff; refl
 
 section
 
-variable (𝕜)
+variables (F) [has_one F] [norm_one_class F]
 
-theorem is_O_with_const_one (c : E) (l : filter α) : is_O_with ∥c∥ l (λ x : α, c) (λ x, (1 : 𝕜)) :=
-begin
-  refine (is_O_with_const_const c _ l).congr_const _,
-  { exact one_ne_zero },
-  { rw [norm_one, div_one] }
-end
+theorem is_O_with_const_one (c : E) (l : filter α) : is_O_with ∥c∥ l (λ x : α, c) (λ x, (1 : F)) :=
+by simp [is_O_with_iff]
 
-theorem is_O_const_one (c : E) (l : filter α) : (λ x : α, c) =O[l] (λ x, (1 : 𝕜)) :=
-(is_O_with_const_one 𝕜 c l).is_O
+theorem is_O_const_one (c : E) (l : filter α) : (λ x : α, c) =O[l] (λ x, (1 : F)) :=
+(is_O_with_const_one F c l).is_O
 
 theorem is_o_const_iff_is_o_one {c : F''} (hc : c ≠ 0) :
-  f =o[l] (λ x, c) ↔ f =o[l] (λ x, (1:𝕜)) :=
-⟨λ h, h.trans_is_O $ is_O_const_one 𝕜 c l, λ h, h.trans_is_O $ is_O_const_const _ hc _⟩
+  f =o[l] (λ x, c) ↔ f =o[l] (λ x, (1 : F)) :=
+⟨λ h, h.trans_is_O_with (is_O_with_const_one _ _ _) (norm_pos_iff.2 hc),
+  λ h, h.trans_is_O $ is_O_const_const _ hc _⟩
+
+@[simp] theorem is_o_one_iff : f' =o[l] (λ x, 1 : α → F) ↔ tendsto f' l (𝓝 0) :=
+by simp only [is_o_iff, norm_one, mul_one, metric.nhds_basis_closed_ball.tendsto_right_iff,
+  metric.mem_closed_ball, dist_zero_right]
+
+@[simp] theorem is_O_one_iff : f =O[l] (λ x, 1 : α → F) ↔ is_bounded_under (≤) l (λ x, ∥f x∥) :=
+by { simp only [is_O_iff, norm_one, mul_one], refl }
+
+alias is_O_one_iff ↔ _ _root_.filter.is_bounded_under.is_O_one
+
+@[simp] theorem is_o_one_left_iff : (λ x, 1 : α → F) =o[l] f ↔ tendsto (λ x, ∥f x∥) l at_top :=
+calc (λ x, 1 : α → F) =o[l] f ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ∥(1 : F)∥ ≤ ∥f x∥ :
+  is_o_iff_nat_mul_le_aux $ or.inl $ λ x, by simp only [norm_one, zero_le_one]
+... ↔ ∀ n : ℕ, true → ∀ᶠ x in l, ∥f x∥ ∈ Ici (n : ℝ) :
+  by simp only [norm_one, mul_one, true_implies_iff, mem_Ici]
+... ↔ tendsto (λ x, ∥f x∥) l at_top : at_top_countable_basis_of_archimedean.1.tendsto_right_iff.symm
+
+theorem _root_.filter.tendsto.is_O_one {c : E'} (h : tendsto f' l (𝓝 c)) :
+  f' =O[l] (λ x, 1 : α → F) :=
+h.norm.is_bounded_under_le.is_O_one F
+
+theorem is_O.trans_tendsto_nhds (hfg : f =O[l] g') {y : F'} (hg : tendsto g' l (𝓝 y)) :
+  f =O[l] (λ x, 1 : α → F) :=
+hfg.trans $ hg.is_O_one F
 
 end
 
 theorem is_o_const_iff {c : F''} (hc : c ≠ 0) :
   f'' =o[l] (λ x, c) ↔ tendsto f'' l (𝓝 0) :=
-(is_o_const_iff_is_o_one ℝ hc).trans
-begin
-  clear hc c,
-  simp only [is_o, is_O_with, norm_one, mul_one, metric.nhds_basis_closed_ball.tendsto_right_iff,
-    metric.mem_closed_ball, dist_zero_right]
-end
+(is_o_const_iff_is_o_one ℝ hc).trans (is_o_one_iff _)
 
 lemma is_o_id_const {c : F''} (hc : c ≠ 0) :
   (λ (x : E''), x) =o[𝓝 0] (λ x, c) :=
 (is_o_const_iff hc).mpr (continuous_id.tendsto 0)
 
 theorem _root_.filter.is_bounded_under.is_O_const (h : is_bounded_under (≤) l (norm ∘ f))
   {c : F''} (hc : c ≠ 0) : f =O[l] (λ x, c) :=
-begin
-  rcases h with ⟨C, hC⟩,
-  refine (is_O.of_bound 1 _).trans (is_O_const_const C hc l),
-  refine (eventually_map.1 hC).mono (λ x h, _),
-  calc ∥f x∥ ≤ C : h
-  ... ≤ abs C : le_abs_self C
-  ... = 1 * ∥C∥ : (one_mul _).symm
-end
+(h.is_O_one ℝ).trans (is_O_const_const _ hc _)
 
 theorem is_O_const_of_tendsto {y : E''} (h : tendsto f'' l (𝓝 y)) {c : F''} (hc : c ≠ 0) :
   f'' =O[l] (λ x, c) :=
@@ -885,14 +941,22 @@ theorem is_O_const_of_ne {c : F''} (hc : c ≠ 0) :
 ⟨λ h, h.is_bounded_under_le, λ h, h.is_O_const hc⟩
 
 theorem is_O_const_iff {c : F''} :
-  f'' =O[l] (λ x, c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ is_bounded_under (≤) l (norm ∘ f'') :=
+  f'' =O[l] (λ x, c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ is_bounded_under (≤) l (λ x, ∥f'' x∥) :=
 begin
   refine ⟨λ h, ⟨λ hc, is_O_zero_right_iff.1 (by rwa ← hc), h.is_bounded_under_le⟩, _⟩,
   rintro ⟨hcf, hf⟩,
   rcases eq_or_ne c 0 with hc|hc,
   exacts [(hcf hc).trans_is_O (is_O_zero _ _), hf.is_O_const hc]
 end
 
+theorem is_O_iff_is_bounded_under_le_div (h : ∀ᶠ x in l, g'' x ≠ 0) :
+  f =O[l] g'' ↔ is_bounded_under (≤) l (λ x, ∥f x∥ / ∥g'' x∥) :=
+begin
+  simp only [is_O_iff, is_bounded_under, is_bounded, eventually_map],
+  exact exists_congr (λ c, eventually_congr $ h.mono $
+    λ x hx, (div_le_iff $ norm_pos_iff.2 hx).symm)
+end
+
 /-- `(λ x, c) =O[l] f` if and only if `f` is bounded away from zero. -/
 lemma is_O_const_left_iff_pos_le_norm {c : E''} (hc : c ≠ 0) :
   (λ x, c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ x in l, b ≤ ∥f' x∥ :=
@@ -912,17 +976,6 @@ section
 
 variable (𝕜)
 
-theorem is_o_one_iff : f'' =o[l] (λ x, (1 : 𝕜)) ↔ tendsto f'' l (𝓝 0) :=
-is_o_const_iff one_ne_zero
-
-theorem is_O_one_of_tendsto {y : E''} (h : tendsto f'' l (𝓝 y)) :
-  f'' =O[l] (λ x, (1:𝕜)) :=
-is_O_const_of_tendsto h one_ne_zero
-
-theorem is_O.trans_tendsto_nhds (hfg : f =O[l] g'') {y : F''} (hg : tendsto g'' l (𝓝 y)) :
-  f =O[l] (λ x, (1:𝕜)) :=
-hfg.trans $ is_O_one_of_tendsto 𝕜 hg
-
 end
 
 theorem is_O.trans_tendsto (hfg : f'' =O[l] g'') (hg : tendsto g'' l (𝓝 0)) :
@@ -1269,18 +1322,10 @@ alias is_o_iff_tendsto' ↔ _ is_o_of_tendsto'
 alias is_o_iff_tendsto ↔ _ is_o_of_tendsto
 
 lemma is_o_const_left_of_ne {c : E''} (hc : c ≠ 0) :
-  (λ x, c) =o[l] g ↔ tendsto (norm ∘ g) l at_top :=
+  (λ x, c) =o[l] g ↔ tendsto (λ x, ∥g x∥) l at_top :=
 begin
-  split; intro h,
-  { refine (at_top_basis' 1).tendsto_right_iff.2 (λ C hC, _),
-    replace hC : 0 < C := zero_lt_one.trans_le hC,
-    replace h : (λ _, 1 : α → ℝ) =o[l] g := (is_O_const_const _ hc _).trans_is_o h,
-    refine (h.def $ inv_pos.2 hC).mono (λ x hx, _),
-    rwa [norm_one, ← div_eq_inv_mul, one_le_div hC] at hx },
-  { suffices : (λ _, 1 : α → ℝ) =o[l] g,
-      from (is_O_const_const c (@one_ne_zero ℝ _ _) _).trans_is_o this,
-    refine is_o_iff.2 (λ ε ε0, (tendsto_at_top.1 h ε⁻¹).mono (λ x hx, _)),
-    rwa [norm_one, ← inv_inv ε, ← div_eq_inv_mul, one_le_div (inv_pos.2 ε0)] }
+  simp only [← is_o_one_left_iff ℝ],
+  exact ⟨(is_O_const_const (1 : ℝ) hc l).trans_is_o, (is_O_const_one ℝ c l).trans_is_o⟩
 end
 
 @[simp] lemma is_o_const_left {c : E''} :
@@ -1434,19 +1479,16 @@ lemma is_o.tendsto_zero_of_tendsto {α E 𝕜 : Type*} [normed_group E] [normed_
 begin
   suffices h : u =o[l] (λ x, (1 : 𝕜)),
   { rwa is_o_one_iff at h },
-  exact huv.trans_is_O (is_O_one_of_tendsto 𝕜 hv),
+  exact huv.trans_is_O (hv.is_O_one 𝕜),
 end
 
 theorem is_o_pow_pow {m n : ℕ} (h : m < n) :
   (λ x : 𝕜, x ^ n) =o[𝓝 0] (λ x, x ^ m) :=
 begin
-  let p := n - m,
-  have nmp : n = m + p := (add_tsub_cancel_of_le (le_of_lt h)).symm,
-  have : (λ(x : 𝕜), x^m) = (λx, x^m * 1), by simp only [mul_one],
-  simp only [this, pow_add, nmp],
-  refine is_O.mul_is_o (is_O_refl _ _) ((is_o_one_iff _).2 _),
-  convert (continuous_pow p).tendsto (0 : 𝕜),
-  exact (zero_pow (tsub_pos_of_lt h)).symm
+  rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩,
+  suffices : (λ x : 𝕜, x ^ m * x ^ p) =o[𝓝 0] (λ x, x ^ m * 1 ^ p),
+    by simpa only [pow_add, one_pow, mul_one],
+  exact is_O.mul_is_o (is_O_refl _ _) (is_o.pow ((is_o_one_iff _).2 tendsto_id) hp0)
 end
 
 theorem is_o_norm_pow_norm_pow {m n : ℕ} (h : m < n) :

src/analysis/calculus/fderiv.lean

@@ -228,7 +228,7 @@ begin
   have : (λ n, c n • (f (x + d n) - f x - f' (d n))) =o[l] (λ n, c n • d n) :=
     (is_O_refl c l).smul_is_o this,
   have : (λ n, c n • (f (x + d n) - f x - f' (d n))) =o[l] (λ n, (1:ℝ)) :=
-    this.trans_is_O (is_O_one_of_tendsto ℝ cdlim),
+    this.trans_is_O (cdlim.is_O_one ℝ),
   have L1 : tendsto (λn, c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0) :=
     (is_o_one_iff ℝ).1 this,
   have L2 : tendsto (λn, f' (c n • d n)) l (𝓝 (f' v)) :=

src/analysis/complex/phragmen_lindelof.lean

@@ -389,8 +389,8 @@ begin
       have hc : continuous_within_at f (Ioi 0 ×ℂ Ioi 0) 0,
       { refine (hd.continuous_on _ _).mono subset_closure,
         simp [closure_re_prod_im, mem_re_prod_im] },
-      refine (is_O_one_of_tendsto ℝ (hc.tendsto.comp $ tendsto_exp_comap_re_at_bot.inf
-        H.tendsto)).trans (is_O_of_le _ (λ w, _)),
+      refine ((hc.tendsto.comp $ tendsto_exp_comap_re_at_bot.inf
+        H.tendsto).is_O_one ℝ).trans (is_O_of_le _ (λ w, _)),
       rw [norm_one, real.norm_of_nonneg (real.exp_pos _).le, real.one_le_exp_iff],
       exact mul_nonneg (le_max_right _ _) (real.exp_pos _).le },
     { -- For the estimate as `ζ.re → ∞`, we reuse the uppoer estimate on `f`