feat(Mathlib/Analysis/SpecificLimits/Basic.lean): add iff versions of…

… lemmas about x^n going to 0 iff x < 1 (#11008)

Add the two iff versions (for NNReals and ENNReals) of the statement that $x^n$ tends to $0$ if and only if $x<1$.



Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -214,6 +214,12 @@ theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1)
 @[deprecated] alias NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 :=
   NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one
 
+@[simp]
+protected theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} :
+    Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 :=
+  ⟨fun h => by simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
+    tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h, tendsto_pow_atTop_nhds_zero_of_lt_one⟩
+
 theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < 1) :
     Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) := by
   rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
@@ -224,6 +230,17 @@ theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r <
 @[deprecated] alias ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 :=
   ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one
 
+@[simp]
+protected theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} :
+    Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by
+  refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩
+  lift r to NNReal
+  · refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))
+    exact eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩
+  rw [← coe_zero] at h
+  norm_cast at h ⊢
+  exact NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h
+
 /-! ### Geometric series-/