[Merged by Bors] - chore(Topology/Algebra/Order/Field): generalize some lemmas to Semifield

Mathlib/Topology/Algebra/Order/Field.lean

@@ -22,6 +22,86 @@ open Set Filter TopologicalSpace Function
 open scoped Pointwise Topology
 open OrderDual (toDual ofDual)
 
+section Semifield
+
+variable {𝕜 α : Type*} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+  [TopologicalSpace 𝕜] [OrderTopology 𝕜]
+  {l : Filter α} {f g : α → 𝕜}
+
+/-- In a linearly ordered semifield with the order topology, if `f` tends to `Filter.atTop` and `g`
+tends to a positive constant `C` then `f * g` tends to `Filter.atTop`. -/
+theorem Filter.Tendsto.atTop_mul_pos {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop)
+    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by
+  refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))
+  filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
+    hf using mul_le_mul_of_nonneg_left hg.le hf
+
+-- TODO: after removing this deprecated alias,
+-- rename `Filter.Tendsto.atTop_mul'` to `Filter.Tendsto.atTop_mul`.
+-- Same for the other 3 similar aliases below.
+@[deprecated (since := "2025-03-18")]
+alias Filter.Tendsto.atTop_mul := Filter.Tendsto.atTop_mul_pos
+
+/-- In a linearly ordered semifield with the order topology, if `f` tends to a positive constant `C`
+and `g` tends to `Filter.atTop` then `f * g` tends to `Filter.atTop`. -/
+theorem Filter.Tendsto.pos_mul_atTop {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
+    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop := by
+  simpa only [mul_comm] using hg.atTop_mul_pos hC hf
+
+@[deprecated (since := "2025-03-18")]
+alias Filter.Tendsto.mul_atTop := Filter.Tendsto.pos_mul_atTop
+
+@[simp]
+lemma inv_atTop₀ : (atTop : Filter 𝕜)⁻¹ = 𝓝[>] 0 :=
+  (((atTop_basis_Ioi' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
+    (nhdsGT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Ioi₀ (inv_pos.2 ha)]
+
+@[simp]
+lemma inv_nhdsGT_zero : (𝓝[>] (0 : 𝕜))⁻¹ = atTop := by rw [← inv_atTop₀, inv_inv]
+
+/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
+theorem tendsto_inv_nhdsGT_zero : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop :=
+  inv_nhdsGT_zero.le
+
+/-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/
+theorem tendsto_inv_atTop_nhdsGT_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝[>] (0 : 𝕜)) :=
+  inv_atTop₀.le
+
+theorem tendsto_inv_atTop_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝 0) :=
+  tendsto_inv_atTop_nhdsGT_zero.mono_right inf_le_left
+
+theorem Filter.Tendsto.inv_tendsto_atTop (h : Tendsto f l atTop) : Tendsto f⁻¹ l (𝓝 0) :=
+  tendsto_inv_atTop_zero.comp h
+
+theorem Filter.Tendsto.inv_tendsto_nhdsGT_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop :=
+  tendsto_inv_nhdsGT_zero.comp h
+
+/-- 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) :
+    Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0) := by
+  simpa only [zpow_neg, zpow_natCast] using (tendsto_pow_atTop (α := 𝕜) hn).inv_tendsto_atTop
+
+theorem tendsto_zpow_atTop_zero {n : ℤ} (hn : n < 0) :
+    Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0) := by
+  lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
+  rw [← neg_pos, ← h, Nat.cast_pos] at hn
+  simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'
+
+-- see Note [lower instance priority]
+instance (priority := 100) IsStrictOrderedRing.toHasContinuousInv₀ [ContinuousMul 𝕜] :
+    HasContinuousInv₀ 𝕜 := .of_nhds_one <| tendsto_order.2 <| by
+  refine ⟨fun x hx => ?_, fun x hx => ?_⟩
+  · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
+      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
+        max_lt hx one_half_lt_one⟩
+    filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
+    exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2
+  · filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
+    exact inv_lt_of_inv_lt₀ (by positivity) hy
+
+end Semifield
+
 /-- If a (possibly non-unital and/or non-associative) ring `R` admits a submultiplicative
 nonnegative norm `norm : R → 𝕜`, where `𝕜` is a linear ordered field, and the open balls
 `{ x | norm x < ε }`, `ε > 0`, form a basis of neighborhoods of zero, then `R` is a topological
@@ -59,29 +139,6 @@ instance (priority := 100) IsStrictOrderedRing.topologicalRing : IsTopologicalRi
   .of_norm abs abs_nonneg (fun _ _ ↦ (abs_mul _ _).le) <| by
     simpa using nhds_basis_abs_sub_lt (0 : 𝕜)
 
-/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g`
-tends to a positive constant `C` then `f * g` tends to `Filter.atTop`. -/
-theorem Filter.Tendsto.atTop_mul_pos {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop)
-    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by
-  refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))
-  filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
-    hf using mul_le_mul_of_nonneg_left hg.le hf
-
--- TODO: after removing this deprecated alias,
--- rename `Filter.Tendsto.atTop_mul'` to `Filter.Tendsto.atTop_mul`.
--- Same for the other 3 similar aliases below.
-@[deprecated (since := "2025-03-18")]
-alias Filter.Tendsto.atTop_mul := Filter.Tendsto.atTop_mul_pos
-
-/-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and
-`g` tends to `Filter.atTop` then `f * g` tends to `Filter.atTop`. -/
-theorem Filter.Tendsto.pos_mul_atTop {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
-    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop := by
-  simpa only [mul_comm] using hg.atTop_mul_pos hC hf
-
-@[deprecated (since := "2025-03-18")]
-alias Filter.Tendsto.mul_atTop := Filter.Tendsto.pos_mul_atTop
-
 /-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g`
 tends to a negative constant `C` then `f * g` tends to `Filter.atBot`. -/
 theorem Filter.Tendsto.atTop_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop)
@@ -128,34 +185,15 @@ theorem Filter.Tendsto.neg_mul_atBot {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (
     (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop := by
   simpa only [mul_comm] using hg.atBot_mul_neg hC hf
 
-@[simp]
-lemma inv_atTop₀ : (atTop : Filter 𝕜)⁻¹ = 𝓝[>] 0 :=
-  (((atTop_basis_Ioi' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
-    (nhdsGT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Ioi₀ (inv_pos.2 ha)]
-
 @[simp]
 lemma inv_atBot₀ : (atBot : Filter 𝕜)⁻¹ = 𝓝[<] 0 :=
   (((atBot_basis_Iio' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
     (nhdsLT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Iio₀ (inv_neg''.2 ha)]
 
-@[simp]
-lemma inv_nhdsGT_zero : (𝓝[>] (0 : 𝕜))⁻¹ = atTop := by rw [← inv_atTop₀, inv_inv]
-
 @[simp]
 lemma inv_nhdsLT_zero : (𝓝[<] (0 : 𝕜))⁻¹ = atBot := by
   rw [← inv_atBot₀, inv_inv]
 
-/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
-theorem tendsto_inv_nhdsGT_zero : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop :=
-  inv_nhdsGT_zero.le
-
-/-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/
-theorem tendsto_inv_atTop_nhdsGT_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝[>] (0 : 𝕜)) :=
-  inv_atTop₀.le
-
-theorem tendsto_inv_atTop_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝 0) :=
-  tendsto_inv_atTop_nhdsGT_zero.mono_right inf_le_left
-
 /-- The function `x ↦ x⁻¹` tends to `-∞` on the left of `0`. -/
 theorem tendsto_inv_nhdsLT_zero : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[<] (0 : 𝕜)) atBot :=
   inv_nhdsLT_zero.le
@@ -191,15 +229,9 @@ lemma Filter.Tendsto.const_div_atBot (hg : Tendsto g l atBot) (r : 𝕜) :
     Tendsto (fun n ↦ r / g n) l (𝓝 0) :=
   tendsto_const_nhds.div_atBot hg
 
-theorem Filter.Tendsto.inv_tendsto_atTop (h : Tendsto f l atTop) : Tendsto f⁻¹ l (𝓝 0) :=
-  tendsto_inv_atTop_zero.comp h
-
 theorem Filter.Tendsto.inv_tendsto_atBot (h : Tendsto f l atBot) : Tendsto f⁻¹ l (𝓝 0) :=
   tendsto_inv_atBot_zero.comp h
 
-theorem Filter.Tendsto.inv_tendsto_nhdsGT_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop :=
-  tendsto_inv_nhdsGT_zero.comp h
-
 theorem Filter.Tendsto.inv_tendsto_nhdsLT_zero (h : Tendsto f l (𝓝[<] 0)) : Tendsto f⁻¹ l atBot :=
   tendsto_inv_nhdsLT_zero.comp h
 
@@ -237,18 +269,6 @@ theorem tendsto_bdd_div_atTop_nhds_zero {f g : α → 𝕜} {b B : 𝕜}
   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) :
-    Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0) := by
-  simpa only [zpow_neg, zpow_natCast] using (tendsto_pow_atTop (α := 𝕜) hn).inv_tendsto_atTop
-
-theorem tendsto_zpow_atTop_zero {n : ℤ} (hn : n < 0) :
-    Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0) := by
-  lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
-  rw [← neg_pos, ← h, Nat.cast_pos] at hn
-  simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'
-
 theorem tendsto_const_mul_zpow_atTop_zero {n : ℤ} {c : 𝕜} (hn : n < 0) :
     Tendsto (fun x => c * x ^ n) atTop (𝓝 0) :=
   mul_zero c ▸ Filter.Tendsto.const_mul c (tendsto_zpow_atTop_zero hn)
@@ -283,20 +303,6 @@ theorem tendsto_const_mul_zpow_atTop_nhds_iff {n : ℤ} {c d : 𝕜} (hc : c ≠
       exact tendsto_const_nhds
     · exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1
 
--- see Note [lower instance priority]
-instance (priority := 100) IsStrictOrderedRing.toHasContinuousInv₀ {𝕜}
-    [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
-    [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] :
-    HasContinuousInv₀ 𝕜 := .of_nhds_one <| tendsto_order.2 <| by
-  refine ⟨fun x hx => ?_, fun x hx => ?_⟩
-  · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
-      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
-        max_lt hx one_half_lt_one⟩
-    filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
-    exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2
-  · filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
-    exact inv_lt_of_inv_lt₀ (by positivity) hy
-
 instance (priority := 100) IsStrictOrderedRing.toIsTopologicalDivisionRing :
     IsTopologicalDivisionRing 𝕜 := ⟨⟩