From 023fc888ae797af73320391bd2ba3907a3232d0d Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 26 Feb 2024 12:06:13 +0100 Subject: [PATCH 1/9] first commit --- Mathlib/Analysis/SpecificLimits/Basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 66986a544eab6..2aff6a3a4318c 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -210,10 +210,18 @@ theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) NNReal.tendsto_coe.1 <| by simp only [NNReal.coe_pow, NNReal.coe_zero, _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr] + #align nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one @[deprecated] alias NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 := NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one +-- @[simp] +-- theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} : +-- Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0)) ↔ r < 1 := 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 + + 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'⟩ From dd0df827bdd154ce108788df300576ec4dc1e798 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 26 Feb 2024 15:23:10 +0100 Subject: [PATCH 2/9] closed main results --- Mathlib/Analysis/SpecificLimits/Basic.lean | 28 +++++++++++++++++----- 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 2aff6a3a4318c..1e574b3749f13 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -215,12 +215,11 @@ 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] --- theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} : --- Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0)) ↔ r < 1 := 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 - +@[simp] +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 @@ -232,6 +231,23 @@ 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 +example (f : ℕ → ℝ≥0∞) (hf : ∀ᶠ x in atTop, f x = 1) : Tendsto f atTop (𝓝 1) := by + exact EventuallyEq.tendsto hf + +@[simp] +theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : + Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by + refine ⟨fun h => ?_, ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one⟩ + have hr : r ≠ ⊤ := by + have : ∀ᶠ n in atTop, (⊤ : ℝ≥0∞)^n = ⊤ := by + simp only [pow_eq_top_iff, ne_eq, true_and, eventually_atTop, ge_iff_le] + exact ⟨1, fun _ _ => by linarith⟩ + exact fun hr => ENNReal.top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto this) (hr ▸ h)) + rw [← ENNReal.coe_zero, ← ENNReal.coe_toNNReal hr] at h + simp_rw [← ENNReal.coe_pow, tendsto_coe, NNReal.tendsto_pow_atTop_nhds_zero_iff, + ← ENNReal.coe_lt_coe, ENNReal.coe_toNNReal hr] at h + exact h + /-! ### Geometric series-/ From c59043a1f9d6bf55103c945d7c21b5a577ef22f5 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 26 Feb 2024 16:58:32 +0100 Subject: [PATCH 3/9] fixed indentation --- Mathlib/Analysis/SpecificLimits/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 1e574b3749f13..7ad0b3d6b4742 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -217,7 +217,7 @@ theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) @[simp] theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} : - Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := + 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⟩ @@ -236,7 +236,7 @@ example (f : ℕ → ℝ≥0∞) (hf : ∀ᶠ x in atTop, f x = 1) : Tendsto f a @[simp] theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : - Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by + Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by refine ⟨fun h => ?_, ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one⟩ have hr : r ≠ ⊤ := by have : ∀ᶠ n in atTop, (⊤ : ℝ≥0∞)^n = ⊤ := by From 5cc7086df8e342a83d5c2beba58e24b763e1b406 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 26 Feb 2024 17:48:11 +0100 Subject: [PATCH 4/9] fixed indentation --- Mathlib/Analysis/SpecificLimits/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 7ad0b3d6b4742..488d64753c1f7 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -236,7 +236,7 @@ example (f : ℕ → ℝ≥0∞) (hf : ∀ᶠ x in atTop, f x = 1) : Tendsto f a @[simp] theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : - Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by + Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by refine ⟨fun h => ?_, ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one⟩ have hr : r ≠ ⊤ := by have : ∀ᶠ n in atTop, (⊤ : ℝ≥0∞)^n = ⊤ := by From 647cd6df35f4b17acec3fff9e17f6797c6736504 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Tue, 27 Feb 2024 17:18:13 +0800 Subject: [PATCH 5/9] Update Basic.lean --- Mathlib/Analysis/SpecificLimits/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 488d64753c1f7..92dcad4fce3f8 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -210,7 +210,6 @@ theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) NNReal.tendsto_coe.1 <| by simp only [NNReal.coe_pow, NNReal.coe_zero, _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr] - #align nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one @[deprecated] alias NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 := NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one From 95bfbfb3266f617c2f63503a698fb9f82a58d29a Mon Sep 17 00:00:00 2001 From: faenuccio Date: Tue, 27 Feb 2024 11:26:09 +0100 Subject: [PATCH 6/9] removed example --- Mathlib/Analysis/SpecificLimits/Basic.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 92dcad4fce3f8..c5ab77b4e8636 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -230,9 +230,6 @@ 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 -example (f : ℕ → ℝ≥0∞) (hf : ∀ᶠ x in atTop, f x = 1) : Tendsto f atTop (𝓝 1) := by - exact EventuallyEq.tendsto hf - @[simp] theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by From 4a1e74d522f588e50bc833ba204b6cbf0c9545d2 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Tue, 27 Feb 2024 11:57:02 +0100 Subject: [PATCH 7/9] Update Mathlib/Analysis/SpecificLimits/Basic.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/Analysis/SpecificLimits/Basic.lean | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index c5ab77b4e8636..e46247949d42b 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -233,16 +233,13 @@ theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < @[simp] theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by - refine ⟨fun h => ?_, ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one⟩ - have hr : r ≠ ⊤ := by - have : ∀ᶠ n in atTop, (⊤ : ℝ≥0∞)^n = ⊤ := by - simp only [pow_eq_top_iff, ne_eq, true_and, eventually_atTop, ge_iff_le] - exact ⟨1, fun _ _ => by linarith⟩ - exact fun hr => ENNReal.top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto this) (hr ▸ h)) - rw [← ENNReal.coe_zero, ← ENNReal.coe_toNNReal hr] at h - simp_rw [← ENNReal.coe_pow, tendsto_coe, NNReal.tendsto_pow_atTop_nhds_zero_iff, - ← ENNReal.coe_lt_coe, ENNReal.coe_toNNReal hr] at h - exact h + 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-/ From 4cf20c00a4db6e5e6299cd0bbee565370d7d75c2 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Tue, 27 Feb 2024 11:57:39 +0100 Subject: [PATCH 8/9] Update Mathlib/Analysis/SpecificLimits/Basic.lean Co-authored-by: Floris van Doorn --- Mathlib/Analysis/SpecificLimits/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index e46247949d42b..f2a8b2392ad64 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -215,7 +215,7 @@ theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one @[simp] -theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} : +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⟩ From 3fd236e8d16c610acd3705e4c1fad86fbb20d057 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Tue, 27 Feb 2024 11:57:48 +0100 Subject: [PATCH 9/9] Update Mathlib/Analysis/SpecificLimits/Basic.lean Co-authored-by: Floris van Doorn --- Mathlib/Analysis/SpecificLimits/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index f2a8b2392ad64..6e7b4832dd538 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -231,7 +231,7 @@ theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one @[simp] -theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : +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