feat(analysis/specific_limits): Lemma for limit of 1 / n as n → ∞ in …

…real algebras (#6249)

This PR introduces a single new lemma about the limit of 1 / n as n → ∞ in the complex numbers. It has been placed in a new file to avoid import creep: the obvious file in which to put it (Analysis.SpecificLimits.Basic) does not have the required imports.
  
Note that this is a prerequisite for an upcoming PR for the Hadamard three-line theorem. Finally, thanks to Patrick Massot for supplying the actual proof on Zulip a while back!



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Mathlib.lean

@@ -820,6 +820,7 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Analysis.SpecificLimits.FloorPow
+import Mathlib.Analysis.SpecificLimits.IsROrC
 import Mathlib.Analysis.SpecificLimits.Normed
 import Mathlib.Analysis.Subadditive
 import Mathlib.Analysis.SumIntegralComparisons

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -53,6 +53,17 @@ theorem tendsto_one_div_add_atTop_nhds_0_nat :
   (tendsto_add_atTop_iff_nat 1).2 (_root_.tendsto_const_div_atTop_nhds_0_nat 1)
 #align tendsto_one_div_add_at_top_nhds_0_nat tendsto_one_div_add_atTop_nhds_0_nat
 
+theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat (𝕜 : Type _) [Semiring 𝕜] [Algebra ℝ≥0 𝕜]
+    [TopologicalSpace 𝕜] [TopologicalSemiring 𝕜] [ContinuousSMul ℝ≥0 𝕜] :
+    Tendsto (algebraMap ℝ≥0 𝕜 ∘ fun n : ℕ => (n : ℝ≥0)⁻¹) atTop (nhds 0) := by
+  convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp tendsto_inverse_atTop_nhds_0_nat
+  rw [map_zero]
+
+theorem tendsto_algebraMap_inverse_atTop_nhds_0_nat (𝕜 : Type _) [Semiring 𝕜] [Algebra ℝ 𝕜]
+    [TopologicalSpace 𝕜] [TopologicalSemiring 𝕜] [ContinuousSMul ℝ 𝕜] :
+    Tendsto (algebraMap ℝ 𝕜 ∘ fun n : ℕ => (n : ℝ)⁻¹) atTop (nhds 0) :=
+  NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat 𝕜
+
 /-- The limit of `n / (n + x)` is 1, for any constant `x` (valid in `ℝ` or any topological division
 algebra over `ℝ`, e.g., `ℂ`).
 

Mathlib/Analysis/SpecificLimits/IsROrC.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2023 Xavier Généreux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Généreux, Patrick Massot
+-/
+import Mathlib.Analysis.SpecificLimits.Basic
+import Mathlib.Analysis.Complex.ReImTopology
+
+/-!
+# A collection of specific limit computations for `IsROrC`
+
+-/
+
+open Set Algebra Filter
+
+variable (𝕜 : Type _) [IsROrC 𝕜]
+
+theorem IsROrC.tendsto_inverse_atTop_nhds_0_nat : 
+    Tendsto (fun n : ℕ => (n : 𝕜)⁻¹) atTop (nhds 0) := by
+  convert tendsto_algebraMap_inverse_atTop_nhds_0_nat 𝕜
+  simp