feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions (#16768)

Used in #15373.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: mariainesdff

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -114,6 +114,53 @@ theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [Topolo
     intros
     simp_all only [comp_apply, map_inv₀, map_natCast]
 
+/-- For any positive `m : ℕ`, `((n % m : ℕ) : ℝ) / (n : ℝ)` tends to `0` as `n` tends to `∞`. -/
+theorem tendsto_mod_div_atTop_nhds_zero_nat {m : ℕ} (hm : 0 < m) :
+    Tendsto (fun n : ℕ => ((n % m : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0) := by
+  have h0 : ∀ᶠ n : ℕ in atTop, 0 ≤ (fun n : ℕ => ((n % m : ℕ) : ℝ)) n := by aesop
+  exact tendsto_bdd_div_atTop_nhds_zero h0
+    (.of_forall (fun n ↦  cast_le.mpr (mod_lt n hm).le)) tendsto_natCast_atTop_atTop
+
+theorem Filter.EventuallyEq.div_mul_cancel {α G : Type*} [GroupWithZero G] {f g : α → G}
+    {l : Filter α} (hg : Tendsto g l (𝓟 {0}ᶜ)) : (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x := by
+  filter_upwards [hg.le_comap <| preimage_mem_comap (m := g) (mem_principal_self {0}ᶜ)] with x hx
+  aesop
+
+/-- If `g` tends to `∞`, then eventually for all `x` we have `(f x / g x) * g x = f x`. -/
+theorem Filter.EventuallyEq.div_mul_cancel_atTop {α K : Type*} [LinearOrderedSemifield K]
+    {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) :
+    (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x :=
+  div_mul_cancel <| hg.mono_right <| le_principal_iff.mpr <|
+    mem_of_superset (Ioi_mem_atTop 0) <| by aesop
+
+/-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
+  constant, then `f` tends to `∞`. -/
+theorem Tendsto.num {α K : Type*} [LinearOrderedField K] [TopologicalSpace K] [OrderTopology K]
+    {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) {a : K} (ha : 0 < a)
+    (hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) :
+    Tendsto f l atTop :=
+  Tendsto.congr' (EventuallyEq.div_mul_cancel_atTop hg) (Tendsto.mul_atTop ha hlim hg)
+
+/-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
+  constant, then `f` tends to `∞`. -/
+theorem Tendsto.den {α K : Type*} [LinearOrderedField K] [TopologicalSpace K] [OrderTopology K]
+    [ContinuousInv K] {f g : α → K} {l : Filter α} (hf : Tendsto f l atTop) {a : K} (ha : 0 < a)
+    (hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) :
+    Tendsto g l atTop := by
+  have hlim' : Tendsto (fun x => g x / f x) l (𝓝 a⁻¹) := by
+    simp_rw [← inv_div (f _)]
+    exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim
+  apply Tendsto.congr' (EventuallyEq.div_mul_cancel_atTop hf)
+    (Tendsto.mul_atTop (inv_pos_of_pos ha) hlim' hf)
+
+/-- If when `x` tends to `∞`, `f x / g x` tends to a positive constant, then `f` tends to `∞` if
+  and only if `g` tends to `∞`. -/
+theorem Tendsto.num_atTop_iff_den_atTop {α K : Type*} [LinearOrderedField K] [TopologicalSpace K]
+    [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α} {a : K} (ha : 0 < a)
+    (hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) :
+    Tendsto f l atTop ↔ Tendsto g l atTop :=
+  ⟨fun hf ↦ Tendsto.den hf ha hlim, fun hg ↦ Tendsto.num hg ha hlim⟩
+
 /-! ### Powers -/
 
 

Mathlib/Data/Set/Pointwise/Interval.lean

@@ -670,6 +670,18 @@ theorem preimage_div_const_uIcc (ha : a ≠ 0) (b c : α) :
     (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]] := by
   simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]
 
+lemma preimage_const_mul_Ioi_or_Iio (hb : a ≠ 0) {U V : Set α}
+    (hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}) (hV : V = HMul.hMul a ⁻¹' U) :
+    V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a} := by
+  obtain ⟨aU, (haU | haU)⟩ := hU <;>
+  simp only [hV, haU, mem_setOf_eq] <;>
+  use a⁻¹ * aU <;>
+  rcases lt_or_gt_of_ne hb with (hb | hb)
+  · right; rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
+  · left; rw [Set.preimage_const_mul_Ioi _ hb, div_eq_inv_mul]
+  · left; rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
+  · right; rw [Set.preimage_const_mul_Iio _ hb, div_eq_inv_mul]
+
 @[simp]
 theorem image_mul_const_uIcc (a b c : α) : (· * a) '' [[b, c]] = [[b * a, c * a]] :=
   if ha : a = 0 then by simp [ha]

Mathlib/Topology/Algebra/Order/Field.lean

@@ -141,6 +141,40 @@ theorem Filter.Tendsto.inv_tendsto_atTop (h : Tendsto f l atTop) : Tendsto f⁻
 theorem Filter.Tendsto.inv_tendsto_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop :=
   tendsto_inv_zero_atTop.comp h
 
+/-- If `g` tends to zero and there exists a constant `C : 𝕜` such that eventually `|f x| ≤ C`,
+  then the product `f * g` tends to zero. -/
+theorem bdd_le_mul_tendsto_zero' {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ x in l, |f x| ≤ C)
+    (hg : Tendsto g l (𝓝 0)) : Tendsto (fun x ↦ f x * g x) l (𝓝 0) := by
+  rw [tendsto_zero_iff_abs_tendsto_zero]
+  have hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0) := by
+    convert (hg.const_mul C).abs
+    simp_rw [mul_zero, abs_zero]
+  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC
+  · filter_upwards [hf] with x _ using abs_nonneg _
+  · filter_upwards [hf] with x hx
+    simp only [comp_apply, abs_mul]
+    exact mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)
+
+/-- If `g` tends to zero and there exist constants `b B : 𝕜` such that eventually `b ≤ f x| ≤ B`,
+  then the product `f * g` tends to zero. -/
+theorem bdd_le_mul_tendsto_zero {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x)
+    (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l (𝓝 0)) :
+    Tendsto (fun x ↦ f x * g x) l (𝓝 0) := by
+  set C := max |b| |B|
+  have hbC : -C ≤ b := neg_le.mpr (le_max_of_le_left (neg_le_abs b))
+  have hBC : B ≤ C := le_max_of_le_right (le_abs_self B)
+  apply bdd_le_mul_tendsto_zero' C _ hg
+  filter_upwards [hb, hB]
+  exact fun x hbx hBx ↦ abs_le.mpr ⟨hbC.trans hbx, hBx.trans hBC⟩
+
+/-- If `g` tends to `atTop` and there exist constants `b B : 𝕜` such that eventually
+  `b ≤ f x| ≤ B`, then the quotient `f / g` tends to zero. -/
+theorem tendsto_bdd_div_atTop_nhds_zero {f g : α → 𝕜} {b B : 𝕜}
+    (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l atTop) :
+    Tendsto (fun x => f x / g x) l (𝓝 0) := by
+  simp only [div_eq_mul_inv]
+  exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop
+
 /-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`.
 A version for positive real powers exists as `tendsto_rpow_neg_atTop`. -/
 theorem tendsto_pow_neg_atTop {n : ℕ} (hn : n ≠ 0) :