chore(topology/algebra/ordered): rename lim*_eq_of_tendsto to tendsto.lim*_eq (#3415)

Also add `tendsto_of_le_liminf_of_limsup_le`

Author: urkud

src/analysis/analytic/basic.lean

@@ -111,7 +111,7 @@ begin
     { simp } },
   have D : liminf at_top (λ n : ℕ, (r : ennreal) / ((C + 1)^(1/(n : ℝ)) : nnreal)) ≤ p.radius :=
     liminf_le_liminf B,
-  rw liminf_eq_of_tendsto filter.at_top_ne_bot L at D,
+  rw L.liminf_eq filter.at_top_ne_bot at D,
   simpa using D
 end
 

src/measure_theory/integration.lean

@@ -1139,26 +1139,14 @@ begin
     limsup at_top (λ (n : ℕ), lintegral (F n)) ≤ ∫⁻ (a : α), limsup at_top (λn, F n a) :
       limsup_lintegral_le hF_meas h_bound h_fin
     ... = lintegral f :
-      lintegral_congr_ae $
-          by filter_upwards [h_lim] assume a h, limsup_eq_of_tendsto at_top_ne_bot h,
+      lintegral_congr_ae $ h_lim.mono $ assume a h, h.limsup_eq at_top_ne_bot,
   have lintegral_le_liminf :=
   calc
     lintegral f = ∫⁻ (a : α), liminf at_top (λ (n : ℕ), F n a) :
-      lintegral_congr_ae $
-      by filter_upwards [h_lim] assume a h, (liminf_eq_of_tendsto at_top_ne_bot h).symm
+      lintegral_congr_ae $ h_lim.mono $ assume a h, (h.liminf_eq at_top_ne_bot).symm
     ... ≤ liminf at_top (λ n, lintegral (F n)) :
       lintegral_liminf_le hF_meas,
-  have liminf_eq_limsup :=
-    le_antisymm
-      (liminf_le_limsup (map_ne_bot at_top_ne_bot))
-      (le_trans limsup_le_lintegral lintegral_le_liminf),
-  have liminf_eq_lintegral : liminf at_top (λ n, lintegral (F n)) = lintegral f :=
-    le_antisymm (by convert limsup_le_lintegral) lintegral_le_liminf,
-  have limsup_eq_lintegral : limsup at_top (λ n, lintegral (F n)) = lintegral f :=
-    le_antisymm
-      limsup_le_lintegral
-      begin convert lintegral_le_liminf, exact liminf_eq_limsup.symm end,
-  exact tendsto_of_liminf_eq_limsup ⟨liminf_eq_lintegral, limsup_eq_lintegral⟩
+  exact tendsto_of_le_liminf_of_limsup_le lintegral_le_liminf limsup_le_lintegral
 end
 
 /-- Dominated convergence theorem for filters with a countable basis -/

src/topology/algebra/ordered.lean

@@ -1797,18 +1797,28 @@ variables [complete_linear_order α] [topological_space α] [order_topology α]
 /-- If the liminf and the limsup of a function coincide, then the limit of the function
 exists and has the same value -/
 theorem tendsto_of_liminf_eq_limsup {f : filter β} {u : β → α} {a : α}
-  (h : liminf f u = a ∧ limsup f u = a) : tendsto u f (𝓝 a) :=
-  le_nhds_of_Limsup_eq_Liminf is_bounded_le_of_top is_bounded_ge_of_bot h.2 h.1
+  (hinf : liminf f u = a) (hsup : limsup f u = a) : tendsto u f (𝓝 a) :=
+le_nhds_of_Limsup_eq_Liminf is_bounded_le_of_top is_bounded_ge_of_bot hsup hinf
+
+/-- If a number `a` is less than or equal to the `liminf` of a function `f` at some filter
+and is greater than or equal to the `limsup` of `f`, then `f` tends to `a` along this filter. -/
+theorem tendsto_of_le_liminf_of_limsup_le {f : filter β} {u : β → α} {a : α}
+  (hinf : a ≤ liminf f u) (hsup : limsup f u ≤ a) :
+  tendsto u f (𝓝 a) :=
+if hf : f = ⊥ then hf.symm ▸ tendsto_bot
+else tendsto_of_liminf_eq_limsup
+  (le_antisymm (le_trans (liminf_le_limsup hf) hsup) hinf)
+  (le_antisymm hsup (le_trans hinf (liminf_le_limsup hf)))
 
 /-- If a function has a limit, then its limsup coincides with its limit-/
-theorem limsup_eq_of_tendsto {f : filter β} {u : β → α} {a : α} (hf : f ≠ ⊥)
+theorem filter.tendsto.limsup_eq {f : filter β} {u : β → α} {a : α} (hf : f ≠ ⊥)
   (h : tendsto u f (𝓝 a)) : limsup f u = a :=
-  Limsup_eq_of_le_nhds (map_ne_bot hf) h
+Limsup_eq_of_le_nhds (map_ne_bot hf) h
 
 /-- If a function has a limit, then its liminf coincides with its limit-/
-theorem liminf_eq_of_tendsto {f : filter β} {u : β → α} {a : α} (hf : f ≠ ⊥)
+theorem filter.tendsto.liminf_eq {f : filter β} {u : β → α} {a : α} (hf : f ≠ ⊥)
   (h : tendsto u f (𝓝 a)) : liminf f u = a :=
-  Liminf_eq_of_le_nhds (map_ne_bot hf) h
+Liminf_eq_of_le_nhds (map_ne_bot hf) h
 
 end complete_linear_order