chore(analysis/asymptotics): a few more lemmas (#5482)

* golf some proofs;
* `x ^ n = o (y ^ n)` as `n → ∞` provided that `0 ≤ x < y`;
* lemmas about `is_O _ _ ⊤` etc;
* if `is_O f g cofinite`, then for some `C>0` and any `x` such that `g x ≠ 0` we have `∥f x∥≤C*∥g x∥`.

src/analysis/asymptotics.lean

@@ -698,6 +698,21 @@ theorem is_O_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α) :
 
 end zero_const
 
+@[simp] lemma is_O_with_top : is_O_with c f g ⊤ ↔ ∀ x, ∥f x∥ ≤ c * ∥g x∥ := iff.rfl
+
+@[simp] lemma is_O_top : is_O f g ⊤ ↔ ∃ C, ∀ x, ∥f x∥ ≤ C * ∥g x∥ := iff.rfl
+
+@[simp] lemma is_o_top : is_o f' g' ⊤ ↔ ∀ x, f' x = 0 :=
+begin
+  refine ⟨_, λ h, (is_o_zero g' ⊤).congr (λ x, (h x).symm) (λ x, rfl)⟩,
+  simp only [is_o_iff, eventually_top],
+  refine λ h x, norm_le_zero_iff.1 _,
+  have : tendsto (λ c : ℝ, c * ∥g' x∥) (𝓝[Ioi 0] 0) (𝓝 0) :=
+    ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left inf_le_left,
+  exact le_of_tendsto_of_tendsto tendsto_const_nhds this
+    (eventually_nhds_within_iff.2 $ eventually_of_forall $ λ c hc, h hc x)
+end
+
 theorem is_O_with_const_one (c : E) (l : filter α) : is_O_with ∥c∥ (λ x : α, c) (λ x, (1 : 𝕜)) l :=
 begin
   refine (is_O_with_const_const c _ l).congr_const _,
@@ -1046,48 +1061,20 @@ have eq₂ : is_O (λ x, g x / g x) (λ x, (1 : 𝕜)) l,
   from is_O_of_le _ (λ x, by by_cases h : ∥g x∥ = 0; simp [h, zero_le_one]),
 (is_o_one_iff 𝕜).mp (eq₁.trans_is_O eq₂)
 
-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,
-  from (is_o_one_iff _).mpr h,
-have eq₂ : is_o (λ x, f x / g x * g x) g l,
-  by convert eq₁.mul_is_O (is_O_refl _ _); simp,
-have eq₃ : is_O f (λ x, f x / g x * g x) l,
-  begin
-    refine is_O_of_le _ (λ x, _),
-    by_cases H : g x = 0,
-    { simp only [H, hgf _ H, mul_zero] },
-    { simp only [div_mul_cancel _ H] }
-  end,
-eq₃.trans_is_o eq₂
-
-private theorem is_o_of_tendsto' {f g : α → 𝕜} {l : filter α}
-    (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) (h : tendsto (λ x, f x / (g x)) l (𝓝 0)) :
-  is_o f g l :=
-let ⟨u, hu, himp⟩ := hgf.exists_mem in
-have key : u.indicator f =ᶠ[l] f,
-  from eventually_eq_of_mem hu eq_on_indicator,
-have himp : ∀ x, g x = 0 → (u.indicator f) x = 0,
-  from λ x hgx,
-    begin
-      by_cases h : x ∈ u,
-      { exact (indicator_of_mem h f).symm ▸ himp x h hgx },
-      { exact indicator_of_not_mem h f }
-    end,
-suffices h : is_o (u.indicator f) g l,
-  from is_o.congr' key (by refl) h,
-is_o_of_tendsto himp (h.congr' (key.symm.div (by refl)))
+theorem is_o_iff_tendsto' {f g : α → 𝕜} {l : filter α}
+    (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
+  is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0) :=
+iff.intro is_o.tendsto_0 $ λ h,
+  (((is_o_one_iff _).mpr h).mul_is_O (is_O_refl g l)).congr'
+    (hgf.mono $ λ x, div_mul_cancel_of_imp) (eventually_of_forall $ λ x, one_mul _)
 
 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 is_o.tendsto_0 (is_o_of_tendsto hgf)
+⟨λ h, h.tendsto_0, (is_o_iff_tendsto' (eventually_of_forall hgf)).2⟩
 
-theorem is_o_iff_tendsto' {f g : α → 𝕜} {l : filter α}
-    (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
-  is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0) :=
-iff.intro is_o.tendsto_0 (is_o_of_tendsto' hgf)
+alias is_o_iff_tendsto' ↔ _ asymptotics.is_o_of_tendsto'
+alias is_o_iff_tendsto ↔ _ asymptotics.is_o_of_tendsto
 
 /-!
 ### Eventually (u / v) * v = u
@@ -1220,6 +1207,34 @@ theorem is_o.right_is_O_add {f₁ f₂ : α → E'} (h : is_o f₁ f₂ l) :
   is_O f₂ (λx, f₁ x + f₂ x) l :=
 ((h.def' one_half_pos).right_le_add_of_lt_1 one_half_lt_one).is_O
 
+/-- If `f x = O(g x)` along `cofinite`, then there exists a positive constant `C` such that
+`∥f x∥ ≤ C * ∥g x∥` whenever `g x ≠ 0`. -/
+theorem bound_of_is_O_cofinite (h : is_O f g' cofinite) :
+  ∃ C > 0, ∀ ⦃x⦄, g' x ≠ 0 → ∥f x∥ ≤ C * ∥g' x∥ :=
+begin
+  rcases h.exists_pos with ⟨C, C₀, hC⟩,
+  rw [is_O_with, eventually_cofinite] at hC,
+  rcases (hC.to_finset.image (λ x, ∥f x∥ / ∥g' x∥)).exists_le with ⟨C', hC'⟩,
+  have : ∀ x, C * ∥g' x∥ < ∥f x∥ → ∥f x∥ / ∥g' x∥ ≤ C', by simpa using hC',
+  refine ⟨max C C', lt_max_iff.2 (or.inl C₀), λ x h₀, _⟩,
+  rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le],
+  exact λ hx, (div_le_iff (norm_pos_iff.2 h₀)).1 (this _ hx)
+end
+
+theorem is_O_cofinite_iff (h : ∀ x, g' x = 0 → f' x = 0) :
+  is_O f' g' cofinite ↔ ∃ C, ∀ x, ∥f' x∥ ≤ C * ∥g' x∥ :=
+⟨λ h', let ⟨C, C₀, hC⟩ := bound_of_is_O_cofinite h' in
+  ⟨C, λ x, if hx : g' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
+  λ h, (is_O_top.2 h).mono le_top⟩
+
+theorem bound_of_is_O_nat_at_top {f : ℕ → E} {g' : ℕ → E'} (h : is_O f g' at_top) :
+  ∃ C > 0, ∀ ⦃x⦄, g' x ≠ 0 → ∥f x∥ ≤ C * ∥g' x∥ :=
+bound_of_is_O_cofinite $ by rwa nat.cofinite_eq_at_top
+
+theorem is_O_nat_at_top_iff {f : ℕ → E'} {g : ℕ → F'} (h : ∀ x, g x = 0 → f x = 0) :
+  is_O f g at_top ↔ ∃ C, ∀ x, ∥f x∥ ≤ C * ∥g x∥ :=
+by rw [← nat.cofinite_eq_at_top, is_O_cofinite_iff h]
+
 end asymptotics
 
 namespace local_homeomorph

src/analysis/specific_limits.lean

@@ -3,19 +3,19 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import analysis.normed_space.basic
 import algebra.geom_sum
 import order.filter.archimedean
 import order.iterate
 import topology.instances.ennreal
 import tactic.ring_exp
+import analysis.asymptotics
 
 /-!
 # A collection of specific limit computations
 -/
 
 noncomputable theory
-open classical function filter finset metric
+open classical function filter finset metric asymptotics
 
 open_locale classical topological_space nat big_operators uniformity nnreal
 
@@ -77,15 +77,30 @@ lemma normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [nor
   tendsto (λ x:𝕜, ∥x⁻¹∥) (𝓝[{x | x ≠ 0}] 0) at_top :=
 (tendsto_inv_zero_at_top.comp tendsto_norm_zero').congr $ λ x, (normed_field.norm_inv x).symm
 
-lemma tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
+lemma tendsto_pow_at_top_nhds_0_of_lt_1 {𝕜 : Type*} [linear_ordered_field 𝕜] [archimedean 𝕜]
+  [topological_space 𝕜] [order_topology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
   tendsto (λn:ℕ, r^n) at_top (𝓝 0) :=
-by_cases
-  (assume : r = 0, (tendsto_add_at_top_iff_nat 1).mp $ by simp [pow_succ, this, tendsto_const_nhds])
-  (assume : r ≠ 0,
+h₁.eq_or_lt.elim
+  (assume : 0 = r, (tendsto_add_at_top_iff_nat 1).mp $ by simp [pow_succ, ← this, tendsto_const_nhds])
+  (assume : 0 < r,
     have tendsto (λn, (r⁻¹ ^ n)⁻¹) at_top (𝓝 0),
       from tendsto_inv_at_top_zero.comp
-        (tendsto_pow_at_top_at_top_of_one_lt $ one_lt_inv (lt_of_le_of_ne h₁ this.symm) h₂),
-    tendsto.congr' (univ_mem_sets' $ by simp *) this)
+        (tendsto_pow_at_top_at_top_of_one_lt $ one_lt_inv this h₂),
+    this.congr (λ n, by simp))
+
+lemma is_o_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) :
+  is_o (λ n : ℕ, r₁ ^ n) (λ n, r₂ ^ n) at_top :=
+have H : 0 < r₂ := h₁.trans_lt h₂,
+is_o_of_tendsto (λ n hn, false.elim $ H.ne' $ pow_eq_zero hn) $
+  (tendsto_pow_at_top_nhds_0_of_lt_1 (div_nonneg h₁ (h₁.trans h₂.le)) ((div_lt_one H).2 h₂)).congr
+    (λ n, div_pow _ _ _)
+
+lemma is_o_pow_pow_of_abs_lt_left {r₁ r₂ : ℝ} (h : abs r₁ < abs r₂) :
+  is_o (λ n : ℕ, r₁ ^ n) (λ n, r₂ ^ n) at_top :=
+begin
+  refine (is_o.of_norm_left _).of_norm_right,
+  exact (is_o_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)
+end
 
 lemma uniformity_basis_dist_pow_of_lt_1 {α : Type*} [metric_space α]
   {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) :
@@ -560,16 +575,14 @@ tendsto_of_tendsto_of_tendsto_of_le_of_le'
   (eventually_of_forall $ λ n, div_nonneg (by exact_mod_cast n.factorial_pos.le)
     (pow_nonneg (by exact_mod_cast n.zero_le) _))
   begin
-    rw eventually_iff_exists_mem,
-    use [set.Ioi 0, Ioi_mem_at_top 0],
-    rintros n (hn : 0 < n),
+    refine (eventually_gt_at_top 0).mono (λ n hn, _),
     rcases nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩,
-    rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div, prod_nat_cast,
-        nat.cast_succ, ← prod_inv_distrib', ← prod_mul_distrib, finset.prod_range_succ'],
+    rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
+      prod_nat_cast, nat.cast_succ, ← prod_inv_distrib', ← prod_mul_distrib,
+      finset.prod_range_succ'],
     simp only [prod_range_succ', one_mul, nat.cast_add, zero_add, nat.cast_one],
     refine mul_le_of_le_one_left (inv_nonneg.mpr $ by exact_mod_cast hn.le) (prod_le_one _ _);
-    intros x hx;
-    rw finset.mem_range at hx,
+      intros x hx; rw finset.mem_range at hx,
     { refine mul_nonneg _ (inv_nonneg.mpr _); norm_cast; linarith },
     { refine (div_le_one $ by exact_mod_cast hn).mpr _, norm_cast, linarith }
   end

src/order/filter/cofinite.lean

@@ -37,6 +37,9 @@ def cofinite : filter α :=
 
 @[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite sᶜ := iff.rfl
 
+@[simp] lemma eventually_cofinite {p : α → Prop} :
+  (∀ᶠ x in cofinite, p x) ↔ finite {x | ¬p x} := iff.rfl
+
 instance cofinite_ne_bot [infinite α] : ne_bot (@cofinite α) :=
 mt empty_in_sets_eq_bot.mpr $ by { simp only [mem_cofinite, compl_empty], exact infinite_univ }