feat(analysis): define asymptotic equivalence of two functions (#4979)

This defines the relation `is_equivalent u v l`, which means that `u-v` is little o of
`v` along the filter `l`. It is required to state, for example, Stirling's formula, or the prime number theorem

src/analysis/asymptotic_equivalent.lean

@@ -0,0 +1,261 @@
+/-
+Copyright (c) 2020 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+import analysis.asymptotics
+import analysis.normed_space.ordered
+import analysis.normed_space.bounded_linear_maps
+
+/-!
+# Asymptotic equivalence
+
+In this file, we define the relation `is_equivalent u v l`, which means that `u-v` is little o of
+`v` along the filter `l`.
+
+Unlike `is_[oO]` relations, this one requires `u` and `v` to have the same codomaine `β`. While the
+definition only requires `β` to be a `normed_group`, most interesting properties require it to be a
+`normed_field`.
+
+## Notations
+
+We introduce the notation `u ~[l] v := is_equivalent u v l`, which you can use by opening the
+`asymptotics` locale.
+
+## Main results
+
+If `β` is a `normed_group` :
+
+- `_ ~[l] _` is an equivalence relation
+- Equivalent statements for `u ~[l] const _ c` :
+  - If `c ≠ 0`, this is true iff `tendsto u l (𝓝 c)` (see `is_equivalent_const_iff_tendsto`)
+  - For `c = 0`, this is true iff `u =ᶠ[l] 0` (see `is_equivalent_zero_iff_eventually_zero`)
+
+If `β` is a `normed_field` :
+
+- Alternative characterization of the relation (see `is_equivalent_iff_exists_eq_mul`) :
+
+  `u ~[l] v ↔ ∃ (φ : α → β) (hφ : tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v`
+
+- Provided some non-vanishing hypothesis, this can be seen as `u ~[l] v ↔ tendsto (u/v) l (𝓝 1)`
+  (see `is_equivalent_iff_tendsto_one`)
+- For any constant `c`, `u ~[l] v` implies `tendsto u l (𝓝 c) ↔ tendsto v l (𝓝 c)`
+  (see `is_equivalent.tendsto_nhds_iff`)
+- `*` and `/` are compatible with `_ ~[l] _` (see `is_equivalent.mul` and `is_equivalent.div`)
+
+If `β` is a `normed_linear_ordered_field` :
+
+- If `u ~[l] v`, we have `tendsto u l at_top ↔ tendsto v l at_top`
+  (see `is_equivalent.tendsto_at_top_iff`)
+
+-/
+
+namespace asymptotics
+
+open filter function
+open_locale topological_space
+
+section normed_group
+
+variables {α β : Type*} [normed_group β]
+
+/-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l` when
+    `u x - v x = o(v x)` as x converges along `l`. -/
+def is_equivalent (u v : α → β) (l : filter α) := is_o (u - v) v l
+
+localized "notation u ` ~[`:50 l:50 `] `:0 v:50 := asymptotics.is_equivalent u v l" in asymptotics
+
+variables {u v w : α → β} {l : filter α}
+
+lemma is_equivalent.is_o (h : u ~[l] v) : is_o (u - v) v l := h
+
+lemma is_equivalent.is_O (h : u ~[l] v) : is_O u v l :=
+(is_O.congr_of_sub h.is_O.symm).mp (is_O_refl _ _)
+
+lemma is_equivalent.is_O_symm (h : u ~[l] v) : is_O v u l :=
+begin
+  convert h.is_o.right_is_O_add,
+  ext,
+  simp
+end
+
+@[refl] lemma is_equivalent.refl : u ~[l] u :=
+begin
+  rw [is_equivalent, sub_self],
+  exact is_o_zero _ _
+end
+
+@[symm] lemma is_equivalent.symm (h : u ~[l] v) : v ~[l] u :=
+(h.is_o.trans_is_O h.is_O_symm).symm
+
+@[trans] lemma is_equivalent.trans (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
+(huv.is_o.trans_is_O hvw.is_O).triangle hvw.is_o
+
+lemma is_equivalent_zero_iff_eventually_zero : u ~[l] 0 ↔ u =ᶠ[l] 0 :=
+begin
+  rw [is_equivalent, sub_zero],
+  exact is_o_zero_right_iff
+end
+
+lemma is_equivalent_const_iff_tendsto {c : β} (h : c ≠ 0) : u ~[l] const _ c ↔ tendsto u l (𝓝 c) :=
+begin
+  rw [is_equivalent, is_o_const_iff h],
+  split; intro h;
+  [ { have := h.add tendsto_const_nhds, rw zero_add at this },
+    { have := h.add tendsto_const_nhds, rw ← sub_self c} ];
+  convert this; ext; simp [sub_eq_add_neg]
+end
+
+lemma is_equivalent.tendsto_const {c : β} (hu : u ~[l] const _ c) : tendsto u l (𝓝 c) :=
+begin
+  rcases (em $ c = 0) with ⟨rfl, h⟩,
+  { exact (tendsto_congr' $ is_equivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds },
+  { exact (is_equivalent_const_iff_tendsto h).mp hu }
+end
+
+lemma is_equivalent.tendsto_nhds {c : β} (huv : u ~[l] v) (hu : tendsto u l (𝓝 c)) :
+  tendsto v l (𝓝 c) :=
+begin
+  by_cases h : c = 0,
+  { rw [h, ← is_o_one_iff ℝ] at *,
+    convert (huv.symm.is_o.trans hu).add hu,
+    simp },
+  { rw ← is_equivalent_const_iff_tendsto h at hu ⊢,
+    exact huv.symm.trans hu }
+end
+
+lemma is_equivalent.tendsto_nhds_iff {c : β} (huv : u ~[l] v) :
+  tendsto u l (𝓝 c) ↔ tendsto v l (𝓝 c) := ⟨huv.tendsto_nhds, huv.symm.tendsto_nhds⟩
+
+end normed_group
+
+open_locale asymptotics
+
+section normed_field
+
+variables {α β : Type*} [normed_field β] {t u v w : α → β} {l : filter α}
+
+lemma is_equivalent_iff_exists_eq_mul : u ~[l] v ↔
+  ∃ (φ : α → β) (hφ : tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v :=
+begin
+  rw [is_equivalent, is_o_iff_exists_eq_mul],
+  split; rintros ⟨φ, hφ, h⟩; [use (φ + 1), use (φ - 1)]; split,
+  { conv in (𝓝 _) { rw ← zero_add (1 : β) },
+    exact hφ.add (tendsto_const_nhds) },
+  { convert h.add (eventually_eq.refl l v); ext; simp [add_mul] },
+  { conv in (𝓝 _) { rw ← sub_self (1 : β) },
+    exact hφ.sub (tendsto_const_nhds) },
+  { convert h.sub (eventually_eq.refl l v); ext; simp [sub_mul] }
+end
+
+lemma is_equivalent.exists_eq_mul (huv : u ~[l] v) :
+  ∃ (φ : α → β) (hφ : tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v :=
+is_equivalent_iff_exists_eq_mul.mp huv
+
+lemma is_equivalent_of_tendsto_one (hz : ∀ᶠ x in l, v x = 0 → u x = 0)
+  (huv : tendsto (u/v) l (𝓝 1)) : u ~[l] v :=
+begin
+  rw is_equivalent_iff_exists_eq_mul,
+  refine ⟨u/v, huv, hz.mono $ λ x hz', (div_mul_cancel_of_imp hz').symm⟩,
+end
+
+lemma is_equivalent_of_tendsto_one' (hz : ∀ x, v x = 0 → u x = 0) (huv : tendsto (u/v) l (𝓝 1)) :
+  u ~[l] v :=
+is_equivalent_of_tendsto_one (eventually_of_forall hz) huv
+
+lemma is_equivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) :
+  u ~[l] v ↔ tendsto (u/v) l (𝓝 1) :=
+begin
+  split,
+  { intro hequiv,
+    have := hequiv.is_o.tendsto_0,
+    simp only [pi.sub_apply, sub_div] at this,
+    have key : tendsto (λ x, v x / v x) l (𝓝 1),
+    { exact (tendsto_congr' $ hz.mono $ λ x hnz, @div_self _ _ (v x) hnz).mpr tendsto_const_nhds },
+    convert this.add key,
+    { ext, simp },
+    { norm_num } },
+  { exact is_equivalent_of_tendsto_one (hz.mono $ λ x hnvz hz, (hnvz hz).elim) }
+end
+
+end normed_field
+
+section smul
+
+lemma is_equivalent.smul {α E 𝕜 : Type*} [normed_field 𝕜] [normed_group E]
+  [normed_space 𝕜 E] {a b : α → 𝕜} {u v : α → E} {l : filter α} (hab : a ~[l] b) (huv : u ~[l] v) :
+  (λ x, a x • u x) ~[l] (λ x, b x • v x) :=
+begin
+  rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩,
+  have : (λ (x : α), a x • u x) - (λ (x : α), b x • v x) =ᶠ[l] λ x, b x • ((φ x • u x) - v x),
+  { convert (habφ.comp₂ (•) $ eventually_eq.refl _ u).sub (eventually_eq.refl _ (λ x, b x • v x)),
+    ext,
+    rw [pi.mul_apply, mul_comm, mul_smul, ← smul_sub] },
+  refine (is_o_congr this.symm $ eventually_eq.refl _ _).mp ((is_O_refl b l).smul_is_o _),
+
+  rcases huv.is_O.exists_pos with ⟨C, hC, hCuv⟩,
+  rw is_equivalent at *,
+  rw is_o_iff at *,
+  rw is_O_with at hCuv,
+  simp only [metric.tendsto_nhds, dist_eq_norm] at hφ,
+  intros c hc,
+  specialize hφ ((c/2)/C) (div_pos (by linarith) hC),
+  specialize huv (show 0 < c/2, by linarith),
+  refine hφ.mp (huv.mp $ hCuv.mono $ λ x hCuvx huvx hφx, _),
+
+  have key :=
+    calc ∥φ x - 1∥ * ∥u x∥
+            ≤ (c/2) / C * ∥u x∥ : mul_le_mul_of_nonneg_right hφx.le (norm_nonneg $ u x)
+        ... ≤ (c/2) / C * (C*∥v x∥) : mul_le_mul_of_nonneg_left hCuvx (div_pos (by linarith) hC).le
+        ... = c/2 * ∥v x∥ : by {field_simp [hC.ne.symm], ring},
+
+  calc ∥((λ (x : α), φ x • u x) - v) x∥
+          = ∥(φ x - 1) • u x + (u x - v x)∥ : by simp [sub_smul, sub_add]
+      ... ≤ ∥(φ x - 1) • u x∥ + ∥u x - v x∥ : norm_add_le _ _
+      ... = ∥φ x - 1∥ * ∥u x∥ + ∥u x - v x∥ : by rw norm_smul
+      ... ≤ c / 2 * ∥v x∥ + ∥u x - v x∥ : add_le_add_right key _
+      ... ≤ c / 2 * ∥v x∥ + c / 2 * ∥v x∥ : add_le_add_left huvx _
+      ... = c * ∥v x∥ : by ring,
+end
+
+end smul
+
+section mul_inv
+
+variables {α β : Type*} [normed_field β] {t u v w : α → β} {l : filter α}
+
+lemma is_equivalent.mul (htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w :=
+htu.smul hvw
+
+lemma is_equivalent.inv (huv : u ~[l] v) : (λ x, (u x)⁻¹) ~[l] (λ x, (v x)⁻¹) :=
+begin
+  rw is_equivalent_iff_exists_eq_mul at *,
+  rcases huv with ⟨φ, hφ, h⟩,
+  rw ← inv_one,
+  refine ⟨λ x, (φ x)⁻¹, tendsto.inv' hφ (by norm_num) , _⟩,
+  convert h.inv,
+  ext,
+  simp [mul_inv']
+end
+
+lemma is_equivalent.div (htu : t ~[l] u) (hvw : v ~[l] w) :
+  (λ x, t x / v x) ~[l] (λ x, u x / w x) :=
+htu.mul hvw.inv
+
+end mul_inv
+
+section normed_linear_ordered_field
+
+variables {α β : Type*} [normed_linear_ordered_field β] {u v : α → β} {l : filter α}
+
+lemma is_equivalent.tendsto_at_top [order_topology β] (huv : u ~[l] v) (hu : tendsto u l at_top) :
+  tendsto v l at_top :=
+let ⟨φ, hφ, h⟩ := huv.symm.exists_eq_mul in
+tendsto.congr' h.symm ((mul_comm u φ) ▸ (tendsto_mul_at_top zero_lt_one hu hφ))
+
+lemma is_equivalent.tendsto_at_top_iff [order_topology β] (huv : u ~[l] v) :
+  tendsto u l at_top ↔ tendsto v l at_top := ⟨huv.tendsto_at_top, huv.symm.tendsto_at_top⟩
+
+end normed_linear_ordered_field
+
+end asymptotics

src/analysis/asymptotics.lean

@@ -1056,11 +1056,33 @@ have eq₃ : is_O f (λ x, f x / g x * g x) l,
   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, 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)
 
+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)
+
 /-!
 ### Eventually (u / v) * v = u
 

src/analysis/normed_space/ordered.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2020 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+import analysis.normed_space.basic
+import algebra.ring.basic
+import analysis.asymptotics
+
+/-!
+# Ordered normed spaces
+
+In this file, we define classes for fields and groups that are both normed and ordered.
+These are mostly useful to avoid diamonds during type class inference.
+-/
+
+open filter asymptotics set
+open_locale topological_space
+
+/-- A `normed_linear_ordered_group` is an additive group that is both a `normed_group` and
+    a `linear_ordered_add_comm_group`. This class is necessary to avoid diamonds. -/
+class normed_linear_ordered_group (α : Type*)
+extends linear_ordered_add_comm_group α, has_norm α, metric_space α :=
+(dist_eq : ∀ x y, dist x y = norm (x - y))
+
+@[priority 100] instance normed_linear_ordered_group.to_normed_group (α : Type*)
+  [normed_linear_ordered_group α] : normed_group α :=
+⟨normed_linear_ordered_group.dist_eq⟩
+
+/-- A `normed_linear_ordered_field` is a field that is both a `normed_field` and a
+    `linear_ordered_field`. This class is necessary to avoid diamonds. -/
+class normed_linear_ordered_field (α : Type*)
+extends linear_ordered_field α, has_norm α, metric_space α :=
+(dist_eq : ∀ x y, dist x y = norm (x - y))
+(norm_mul' : ∀ a b, norm (a * b) = norm a * norm b)
+
+@[priority 100] instance normed_linear_ordered_field.to_normed_field (α : Type*)
+  [normed_linear_ordered_field α] : normed_field α :=
+{ dist_eq := normed_linear_ordered_field.dist_eq,
+  norm_mul' := normed_linear_ordered_field.norm_mul' }
+
+@[priority 100] instance normed_linear_ordered_field.to_normed_linear_ordered_group (α : Type*)
+[normed_linear_ordered_field α] : normed_linear_ordered_group α :=
+⟨normed_linear_ordered_field.dist_eq⟩
+
+lemma tendsto_pow_div_pow_at_top_of_lt {α : Type*} [normed_linear_ordered_field α]
+  [order_topology α] {p q : ℕ} (hpq : p < q) :
+  tendsto (λ (x : α), x^p / x^q) at_top (𝓝 0) :=
+begin
+  suffices h : tendsto (λ (x : α), x ^ ((p : ℤ) - q)) at_top (𝓝 0),
+  { refine (tendsto_congr' ((eventually_gt_at_top (0 : α)).mono (λ x hx, _))).mp h,
+    simp [fpow_sub hx.ne.symm] },
+  rw ← neg_sub,
+  rw ← int.coe_nat_sub hpq.le,
+  have : 1 ≤ q - p := nat.sub_pos_of_lt hpq,
+  exact @tendsto_pow_neg_at_top α _ _ (by apply_instance) _ this,
+end
+
+lemma is_o_pow_pow_at_top_of_lt {α : Type} [normed_linear_ordered_field α]
+  [order_topology α] {p q : ℕ} (hpq : p < q) :
+  is_o (λ (x : α), x^p) (λ (x : α), x^q) at_top :=
+begin
+  refine (is_o_iff_tendsto' _).mpr (tendsto_pow_div_pow_at_top_of_lt hpq),
+  rw eventually_iff_exists_mem,
+  exact ⟨Ioi 0, Ioi_mem_at_top 0, λ x (hx : 0 < x) hxq, (pow_ne_zero q hx.ne.symm hxq).elim⟩,
+end