chore(Analysis/SpecificLimits/Normed): move lemmas earlier (#18046)

These lemmas can be proved earlier at no cost.

This is one step towards reducing imports in this area of mathlib.

Author: YaelDillies

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -2048,4 +2048,12 @@ end IsBigORev
 
 end ContinuousOn
 
+/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero. -/
+lemma NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι 𝕜 𝔸 : Type*}
+    [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [BoundedSMul 𝕜 𝔸] {l : Filter ι}
+    {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Tendsto ε l (𝓝 0)) (hf : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) :
+    Tendsto (ε • f) l (𝓝 0) := by
+  rw [← isLittleO_one_iff 𝕜] at hε ⊢
+  simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))
+
 set_option linter.style.longFile 2200

Mathlib/Analysis/Normed/Field/InfiniteSum.lean

@@ -164,3 +164,10 @@ theorem hasSum_sum_range_mul_of_summable_norm' {f g : ℕ → R}
   exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' hf h'f hg h'g
 
 end Nat
+
+lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
+    (∃ r, Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)) → Summable f
+  | ⟨r, hr⟩ => by
+    refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
+    · exact fun i ↦ norm_nonneg _
+    · simpa only using hr

Mathlib/Analysis/Normed/Field/Lemmas.lean

@@ -320,6 +320,19 @@ example [Monoid β] (φ : β →* α) {x : β} {k : ℕ+} (h : x ^ (k : ℕ) = 1
 @[simp] lemma AddChar.norm_apply {G : Type*} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α)
     (x : G) : ‖ψ x‖ = 1 := (ψ.toMonoidHom.isOfFinOrder <| isOfFinOrder_of_finite _).norm_eq_one
 
+lemma NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop :
+    Tendsto (fun x : α ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop :=
+  (tendsto_inv_zero_atTop.comp tendsto_norm_zero').congr fun x ↦ (norm_inv x).symm
+
+lemma NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop {m : ℤ} (hm : m < 0) :
+    Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop := by
+  obtain ⟨m, rfl⟩ := neg_surjective m
+  rw [neg_lt_zero] at hm
+  lift m to ℕ using hm.le
+  rw [Int.natCast_pos] at hm
+  simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow]
+  exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop
+
 end NormedDivisionRing
 
 namespace NormedField
@@ -361,6 +374,22 @@ theorem denseRange_nnnorm : DenseRange (nnnorm : α → ℝ≥0) :=
 
 end Densely
 
+section NontriviallyNormedField
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : ℤ} {x : 𝕜}
+
+@[simp]
+protected lemma continuousAt_zpow : ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n := by
+  refine ⟨?_, continuousAt_zpow₀ _ _⟩
+  contrapose!
+  rintro ⟨rfl, hm⟩ hc
+  exact not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
+    (tendsto_norm_zpow_nhdsWithin_0_atTop hm)
+
+@[simp]
+protected lemma continuousAt_inv : ContinuousAt Inv.inv x ↔ x ≠ 0 := by
+  simpa using NormedField.continuousAt_zpow (n := -1) (x := x)
+
+end NontriviallyNormedField
 end NormedField
 
 namespace NNReal

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -773,7 +773,8 @@ theorem tendsto_norm_div_self (x : E) : Tendsto (fun a => ‖a / x‖) (𝓝 x)
 theorem tendsto_norm' {x : E} : Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖) := by
   simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)
 
-@[to_additive]
+/-- See `tendsto_norm_one` for a version with pointed neighborhoods. -/
+@[to_additive "See `tendsto_norm_zero` for a version with pointed neighborhoods."]
 theorem tendsto_norm_one : Tendsto (fun a : E => ‖a‖) (𝓝 1) (𝓝 0) := by
   simpa using tendsto_norm_div_self (1 : E)
 
@@ -1283,6 +1284,11 @@ theorem nnnorm_ne_zero_iff' : ‖a‖₊ ≠ 0 ↔ a ≠ 1 :=
 @[to_additive (attr := simp) nnnorm_pos]
 lemma nnnorm_pos' : 0 < ‖a‖₊ ↔ a ≠ 1 := pos_iff_ne_zero.trans nnnorm_ne_zero_iff'
 
+/-- See `tendsto_norm_one` for a version with full neighborhoods. -/
+@[to_additive "See `tendsto_norm_zero` for a version with full neighborhoods."]
+lemma tendsto_norm_one' : Tendsto (norm : E → ℝ) (𝓝[≠] 1) (𝓝[>] 0) :=
+  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff''.2 hx
+
 @[to_additive]
 theorem tendsto_norm_div_self_punctured_nhds (a : E) :
     Tendsto (fun x => ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0) :=
@@ -1414,3 +1420,5 @@ instance (priority := 75) normedCommGroup [NormedCommGroup E] {S : Type*} [SetLi
   NormedCommGroup.induced _ _ (SubgroupClass.subtype s) Subtype.coe_injective
 
 end SubgroupClass
+
+lemma tendsto_norm_atTop_atTop : Tendsto (norm : ℝ → ℝ) atTop atTop := tendsto_abs_atTop_atTop

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -28,60 +28,8 @@ open Set Function Filter Finset Metric Asymptotics Topology Nat NNReal ENNReal
 
 variable {α β ι : Type*}
 
-theorem tendsto_norm_atTop_atTop : Tendsto (norm : ℝ → ℝ) atTop atTop :=
-  tendsto_abs_atTop_atTop
-
-theorem summable_of_absolute_convergence_real {f : ℕ → ℝ} :
-    (∃ r, Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)) → Summable f
-  | ⟨r, hr⟩ => by
-    refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
-    · exact fun i ↦ norm_nonneg _
-    · simpa only using hr
-
 /-! ### Powers -/
 
-
-theorem tendsto_norm_zero' {𝕜 : Type*} [NormedAddCommGroup 𝕜] :
-    Tendsto (norm : 𝕜 → ℝ) (𝓝[≠] 0) (𝓝[>] 0) :=
-  tendsto_norm_zero.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff.2 hx
-
-namespace NormedField
-
-theorem tendsto_norm_inverse_nhdsWithin_0_atTop {𝕜 : Type*} [NormedDivisionRing 𝕜] :
-    Tendsto (fun x : 𝕜 ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop :=
-  (tendsto_inv_zero_atTop.comp tendsto_norm_zero').congr fun x ↦ (norm_inv x).symm
-
-theorem tendsto_norm_zpow_nhdsWithin_0_atTop {𝕜 : Type*} [NormedDivisionRing 𝕜] {m : ℤ}
-    (hm : m < 0) :
-    Tendsto (fun x : 𝕜 ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop := by
-  rcases neg_surjective m with ⟨m, rfl⟩
-  rw [neg_lt_zero] at hm; lift m to ℕ using hm.le; rw [Int.natCast_pos] at hm
-  simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow]
-  exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop
-
-/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero. -/
-theorem tendsto_zero_smul_of_tendsto_zero_of_bounded {ι 𝕜 𝔸 : Type*} [NormedDivisionRing 𝕜]
-    [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [BoundedSMul 𝕜 𝔸] {l : Filter ι} {ε : ι → 𝕜} {f : ι → 𝔸}
-    (hε : Tendsto ε l (𝓝 0)) (hf : Filter.IsBoundedUnder (· ≤ ·) l (norm ∘ f)) :
-    Tendsto (ε • f) l (𝓝 0) := by
-  rw [← isLittleO_one_iff 𝕜] at hε ⊢
-  simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))
-
-@[simp]
-theorem continuousAt_zpow {𝕜 : Type*} [NontriviallyNormedField 𝕜] {m : ℤ} {x : 𝕜} :
-    ContinuousAt (fun x ↦ x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m := by
-  refine ⟨?_, continuousAt_zpow₀ _ _⟩
-  contrapose!; rintro ⟨rfl, hm⟩ hc
-  exact not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
-    (tendsto_norm_zpow_nhdsWithin_0_atTop hm)
-
-@[simp]
-theorem continuousAt_inv {𝕜 : Type*} [NontriviallyNormedField 𝕜] {x : 𝕜} :
-    ContinuousAt Inv.inv x ↔ x ≠ 0 := by
-  simpa [(zero_lt_one' ℤ).not_le] using @continuousAt_zpow _ _ (-1) x
-
-end NormedField
-
 theorem isLittleO_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) :
     (fun n : ℕ ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n :=
   have H : 0 < r₂ := h₁.trans_lt h₂