From 856cfd48476696148040e15ccb6cc1557cdd070b Mon Sep 17 00:00:00 2001
From: Oliver Nash <github@olivernash.org>
Date: Thu, 13 Oct 2022 11:47:25 +0000
Subject: [PATCH] feat(order/liminf_limsup): define `filter.blimsup`,
 `filter.bliminf` (#16819)

Also characterise `cofinite.limsup` and `cofinite.liminf` for the lattice of sets.
---
 src/analysis/analytic/radius_liminf.lean      |   2 +-
 src/analysis/normed_space/spectrum.lean       |   5 +-
 .../constructions/borel_space.lean            |  12 +-
 src/measure_theory/function/lp_space.lean     |  14 +-
 src/measure_theory/integral/lebesgue.lean     |  18 +-
 .../finite_measure_weak_convergence.lean      |   4 +-
 src/measure_theory/measure/hausdorff.lean     |  14 +-
 src/measure_theory/measure/measure_space.lean |   4 +-
 src/order/liminf_limsup.lean                  | 320 ++++++++++++++----
 .../martingale/borel_cantelli.lean            |   2 +-
 src/probability/martingale/convergence.lean   |   2 +-
 src/topology/algebra/order/liminf_limsup.lean |  14 +-
 src/topology/instances/ennreal.lean           |  12 +-
 .../metric_space/hausdorff_dimension.lean     |   4 +-
 14 files changed, 302 insertions(+), 125 deletions(-)

diff --git a/src/analysis/analytic/radius_liminf.lean b/src/analysis/analytic/radius_liminf.lean
index 429adbf102d1a..d3f1220e00408 100644
--- a/src/analysis/analytic/radius_liminf.lean
+++ b/src/analysis/analytic/radius_liminf.lean
@@ -27,7 +27,7 @@ variables (p : formal_multilinear_series 𝕜 E F)
 /-- The radius of a formal multilinear series is equal to
 $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{∥p n∥}}$. The actual statement uses `ℝ≥0` and some
 coercions. -/
-lemma radius_eq_liminf : p.radius = liminf at_top (λ n, 1/((∥p n∥₊) ^ (1 / (n : ℝ)) : ℝ≥0)) :=
+lemma radius_eq_liminf : p.radius = liminf (λ n, 1/((∥p n∥₊) ^ (1 / (n : ℝ)) : ℝ≥0)) at_top :=
 begin
   have : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n →
     ((r : ℝ≥0∞) ≤ 1 / ↑(∥p n∥₊ ^ (1 / (n : ℝ))) ↔ ∥p n∥₊ * r ^ n ≤ 1),
diff --git a/src/analysis/normed_space/spectrum.lean b/src/analysis/normed_space/spectrum.lean
index 367d2fcbb12c6..cd7c42335f53d 100644
--- a/src/analysis/normed_space/spectrum.lean
+++ b/src/analysis/normed_space/spectrum.lean
@@ -312,7 +312,7 @@ variables
 
 /-- The `limsup` relationship for the spectral radius used to prove `spectrum.gelfand_formula`. -/
 lemma limsup_pow_nnnorm_pow_one_div_le_spectral_radius (a : A) :
-  limsup at_top (λ n : ℕ, ↑∥a ^ n∥₊ ^ (1 / n : ℝ)) ≤ spectral_radius ℂ a :=
+  limsup (λ n : ℕ, ↑∥a ^ n∥₊ ^ (1 / n : ℝ)) at_top ≤ spectral_radius ℂ a :=
 begin
   refine ennreal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt (λ r r_pos r_lt, _)),
   simp_rw [inv_limsup, ←one_div],
@@ -321,7 +321,8 @@ begin
   suffices h : (r : ℝ≥0∞) ≤ p.radius,
   { convert h,
     simp only [p.radius_eq_liminf, ←norm_to_nnreal, norm_mk_pi_field],
-    refine congr_arg _ (funext (λ n, congr_arg _ _)),
+    congr,
+    ext n,
     rw [norm_to_nnreal, ennreal.coe_rpow_def (∥a ^ n∥₊) (1 / n : ℝ), if_neg],
     exact λ ha, by linarith [ha.2, (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ))], },
   { have H₁ := (differentiable_on_inverse_one_sub_smul r_lt).has_fpower_series_on_ball r_pos,
diff --git a/src/measure_theory/constructions/borel_space.lean b/src/measure_theory/constructions/borel_space.lean
index 58fb2f7ca3b3d..341d5e46b0317 100644
--- a/src/measure_theory/constructions/borel_space.lean
+++ b/src/measure_theory/constructions/borel_space.lean
@@ -1243,7 +1243,7 @@ end
 -/
 lemma measurable_liminf' {ι ι'} {f : ι → δ → α} {u : filter ι} (hf : ∀ i, measurable (f i))
   {p : ι' → Prop} {s : ι' → set ι} (hu : u.has_countable_basis p s) (hs : ∀ i, (s i).countable) :
-  measurable (λ x, liminf u (λ i, f i x)) :=
+  measurable (λ x, liminf (λ i, f i x) u) :=
 begin
   simp_rw [hu.to_has_basis.liminf_eq_supr_infi],
   refine measurable_bsupr _ hu.countable _,
@@ -1254,7 +1254,7 @@ end
 -/
 lemma measurable_limsup' {ι ι'}  {f : ι → δ → α} {u : filter ι} (hf : ∀ i, measurable (f i))
   {p : ι' → Prop} {s : ι' → set ι} (hu : u.has_countable_basis p s) (hs : ∀ i, (s i).countable) :
-  measurable (λ x, limsup u (λ i, f i x)) :=
+  measurable (λ x, limsup (λ i, f i x) u) :=
 begin
   simp_rw [hu.to_has_basis.limsup_eq_infi_supr],
   refine measurable_binfi _ hu.countable _,
@@ -1265,14 +1265,14 @@ end
 -/
 @[measurability]
 lemma measurable_liminf {f : ℕ → δ → α} (hf : ∀ i, measurable (f i)) :
-  measurable (λ x, liminf at_top (λ i, f i x)) :=
+  measurable (λ x, liminf (λ i, f i x) at_top) :=
 measurable_liminf' hf at_top_countable_basis (λ i, to_countable _)
 
 /-- `limsup` over `ℕ` is measurable. See `measurable_limsup'` for a version with a general filter.
 -/
 @[measurability]
 lemma measurable_limsup {f : ℕ → δ → α} (hf : ∀ i, measurable (f i)) :
-  measurable (λ x, limsup at_top (λ i, f i x)) :=
+  measurable (λ x, limsup (λ i, f i x) at_top) :=
 measurable_limsup' hf at_top_countable_basis (λ i, to_countable _)
 
 end complete_linear_order
@@ -1900,10 +1900,10 @@ lemma measurable_of_tendsto_ennreal' {ι} {f : ι → α → ℝ≥0∞} {g : α
 begin
   rcases u.exists_seq_tendsto with ⟨x, hx⟩,
   rw [tendsto_pi_nhds] at lim,
-  have : (λ y, liminf at_top (λ n, (f (x n) y : ℝ≥0∞))) = g :=
+  have : (λ y, liminf (λ n, (f (x n) y : ℝ≥0∞)) at_top) = g :=
     by { ext1 y, exact ((lim y).comp hx).liminf_eq, },
   rw ← this,
-  show measurable (λ y, liminf at_top (λ n, (f (x n) y : ℝ≥0∞))),
+  show measurable (λ y, liminf (λ n, (f (x n) y : ℝ≥0∞)) at_top),
   exact measurable_liminf (λ n, hf (x n)),
 end
 
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
index 5d38b024c5ccf..bd581d859eecb 100644
--- a/src/measure_theory/function/lp_space.lean
+++ b/src/measure_theory/function/lp_space.lean
@@ -1433,7 +1433,7 @@ variables [measurable_space E] [opens_measurable_space E] {R : ℝ≥0}
 
 lemma ae_bdd_liminf_at_top_rpow_of_snorm_bdd {p : ℝ≥0∞}
   {f : ℕ → α → E} (hfmeas : ∀ n, measurable (f n)) (hbdd : ∀ n, snorm (f n) p μ ≤ R) :
-  ∀ᵐ x ∂μ, liminf at_top (λ n, (∥f n x∥₊ ^ p.to_real : ℝ≥0∞)) < ∞ :=
+  ∀ᵐ x ∂μ, liminf (λ n, (∥f n x∥₊ ^ p.to_real : ℝ≥0∞)) at_top < ∞ :=
 begin
   by_cases hp0 : p.to_real = 0,
   { simp only [hp0, ennreal.rpow_zero],
@@ -1456,7 +1456,7 @@ end
 
 lemma ae_bdd_liminf_at_top_of_snorm_bdd {p : ℝ≥0∞} (hp : p ≠ 0)
   {f : ℕ → α → E} (hfmeas : ∀ n, measurable (f n)) (hbdd : ∀ n, snorm (f n) p μ ≤ R) :
-  ∀ᵐ x ∂μ, liminf at_top (λ n, (∥f n x∥₊ : ℝ≥0∞)) < ∞ :=
+  ∀ᵐ x ∂μ, liminf (λ n, (∥f n x∥₊ : ℝ≥0∞)) at_top < ∞ :=
 begin
   by_cases hp' : p = ∞,
   { subst hp',
@@ -1470,14 +1470,14 @@ begin
       (ennreal.add_lt_top.2 ⟨ennreal.coe_lt_top, ennreal.one_lt_top⟩) },
   filter_upwards [ae_bdd_liminf_at_top_rpow_of_snorm_bdd hfmeas hbdd] with x hx,
   have hppos : 0 < p.to_real := ennreal.to_real_pos hp hp',
-  have : liminf at_top (λ n, (∥f n x∥₊ ^ p.to_real : ℝ≥0∞)) =
-    liminf at_top (λ n, (∥f n x∥₊ : ℝ≥0∞)) ^ p.to_real,
-  { change liminf at_top (λ n, ennreal.order_iso_rpow p.to_real hppos (∥f n x∥₊ : ℝ≥0∞)) =
-      ennreal.order_iso_rpow p.to_real hppos (liminf at_top (λ n, (∥f n x∥₊ : ℝ≥0∞))),
+  have : liminf (λ n, (∥f n x∥₊ ^ p.to_real : ℝ≥0∞)) at_top =
+    (liminf (λ n, (∥f n x∥₊ : ℝ≥0∞)) at_top)^ p.to_real,
+  { change liminf (λ n, ennreal.order_iso_rpow p.to_real hppos (∥f n x∥₊ : ℝ≥0∞)) at_top =
+      ennreal.order_iso_rpow p.to_real hppos (liminf (λ n, (∥f n x∥₊ : ℝ≥0∞)) at_top),
     refine (order_iso.liminf_apply (ennreal.order_iso_rpow p.to_real _) _ _ _ _).symm;
     is_bounded_default },
   rw this at hx,
-  rw [← ennreal.rpow_one (liminf at_top (λ n, ∥f n x∥₊)), ← mul_inv_cancel hppos.ne.symm,
+  rw [← ennreal.rpow_one (liminf (λ n, ∥f n x∥₊) at_top), ← mul_inv_cancel hppos.ne.symm,
     ennreal.rpow_mul],
   exact ennreal.rpow_lt_top_of_nonneg (inv_nonneg.2 hppos.le) hx.ne,
 end
diff --git a/src/measure_theory/integral/lebesgue.lean b/src/measure_theory/integral/lebesgue.lean
index c60e524d6800d..f660c99b69315 100644
--- a/src/measure_theory/integral/lebesgue.lean
+++ b/src/measure_theory/integral/lebesgue.lean
@@ -1866,9 +1866,9 @@ lintegral_infi_ae h_meas (λ n, ae_of_all _ $ h_anti n.le_succ) h_fin
 
 /-- Known as Fatou's lemma, version with `ae_measurable` functions -/
 lemma lintegral_liminf_le' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀n, ae_measurable (f n) μ) :
-  ∫⁻ a, liminf at_top (λ n, f n a) ∂μ ≤ liminf at_top (λ n, ∫⁻ a, f n a ∂μ) :=
+  ∫⁻ a, liminf (λ n, f n a) at_top ∂μ ≤ liminf (λ n, ∫⁻ a, f n a ∂μ) at_top :=
 calc
-  ∫⁻ a, liminf at_top (λ n, f n a) ∂μ = ∫⁻ a, ⨆n:ℕ, ⨅i≥n, f i a ∂μ :
+  ∫⁻ a, liminf (λ n, f n a) at_top ∂μ = ∫⁻ a, ⨆n:ℕ, ⨅i≥n, f i a ∂μ :
      by simp only [liminf_eq_supr_infi_of_nat]
   ... = ⨆n:ℕ, ∫⁻ a, ⨅i≥n, f i a ∂μ :
     lintegral_supr'
@@ -1880,14 +1880,14 @@ calc
 
 /-- Known as Fatou's lemma -/
 lemma lintegral_liminf_le {f : ℕ → α → ℝ≥0∞} (h_meas : ∀n, measurable (f n)) :
-  ∫⁻ a, liminf at_top (λ n, f n a) ∂μ ≤ liminf at_top (λ n, ∫⁻ a, f n a ∂μ) :=
+  ∫⁻ a, liminf (λ n, f n a) at_top ∂μ ≤ liminf (λ n, ∫⁻ a, f n a ∂μ) at_top :=
 lintegral_liminf_le' (λ n, (h_meas n).ae_measurable)
 
 lemma limsup_lintegral_le {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞}
   (hf_meas : ∀ n, measurable (f n)) (h_bound : ∀n, f n ≤ᵐ[μ] g) (h_fin : ∫⁻ a, g a ∂μ ≠ ∞) :
-  limsup at_top (λn, ∫⁻ a, f n a ∂μ) ≤ ∫⁻ a, limsup at_top (λn, f n a) ∂μ :=
+  limsup (λn, ∫⁻ a, f n a ∂μ) at_top ≤ ∫⁻ a, limsup (λn, f n a) at_top ∂μ :=
 calc
-  limsup at_top (λn, ∫⁻ a, f n a ∂μ) = ⨅n:ℕ, ⨆i≥n, ∫⁻ a, f i a ∂μ :
+  limsup (λn, ∫⁻ a, f n a ∂μ) at_top = ⨅n:ℕ, ⨆i≥n, ∫⁻ a, f i a ∂μ :
     limsup_eq_infi_supr_of_nat
   ... ≤ ⨅n:ℕ, ∫⁻ a, ⨆i≥n, f i a ∂μ :
     infi_mono $ assume n, supr₂_lintegral_le _
@@ -1900,7 +1900,7 @@ calc
         refine (ae_all_iff.2 h_bound).mono (λ n hn, _),
         exact supr_le (λ i, supr_le $ λ hi, hn i) }
     end
-  ... = ∫⁻ a, limsup at_top (λn, f n a) ∂μ :
+  ... = ∫⁻ a, limsup (λn, f n a) at_top ∂μ :
     by simp only [limsup_eq_infi_supr_of_nat]
 
 /-- Dominated convergence theorem for nonnegative functions -/
@@ -1911,10 +1911,10 @@ lemma tendsto_lintegral_of_dominated_convergence
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
   tendsto (λn, ∫⁻ a, F n a ∂μ) at_top (𝓝 (∫⁻ a, f a ∂μ)) :=
 tendsto_of_le_liminf_of_limsup_le
-(calc ∫⁻ a, f a ∂μ = ∫⁻ a, liminf at_top (λ (n : ℕ), F n a) ∂μ :
+(calc ∫⁻ a, f a ∂μ = ∫⁻ a, liminf (λ (n : ℕ), F n a) at_top ∂μ :
       lintegral_congr_ae $ h_lim.mono $ assume a h, h.liminf_eq.symm
- ... ≤ liminf at_top (λ n, ∫⁻ a, F n a ∂μ) : lintegral_liminf_le hF_meas)
-(calc limsup at_top (λ (n : ℕ), ∫⁻ a, F n a ∂μ) ≤ ∫⁻ a, limsup at_top (λn, F n a) ∂μ :
+ ... ≤ liminf (λ n, ∫⁻ a, F n a ∂μ) at_top : lintegral_liminf_le hF_meas)
+(calc limsup (λ (n : ℕ), ∫⁻ a, F n a ∂μ) at_top ≤ ∫⁻ a, limsup (λn, F n a) at_top ∂μ :
       limsup_lintegral_le hF_meas h_bound h_fin
  ... = ∫⁻ a, f a ∂μ : lintegral_congr_ae $ h_lim.mono $ λ a h, h.limsup_eq)
 
diff --git a/src/measure_theory/measure/finite_measure_weak_convergence.lean b/src/measure_theory/measure/finite_measure_weak_convergence.lean
index 7f16b36478e8a..849b1b8ff57bd 100644
--- a/src/measure_theory/measure/finite_measure_weak_convergence.lean
+++ b/src/measure_theory/measure/finite_measure_weak_convergence.lean
@@ -1063,7 +1063,7 @@ lemma le_measure_compl_liminf_of_limsup_measure_le
 begin
   by_cases L_bot : L = ⊥,
   { simp only [L_bot, le_top,
-      (show liminf ⊥ (λ i, μs i Eᶜ) = ⊤, by simp only [liminf, filter.map_bot, Liminf_bot])], },
+      (show liminf (λ i, μs i Eᶜ) ⊥ = ⊤, by simp only [liminf, filter.map_bot, Liminf_bot])], },
   haveI : L.ne_bot, from {ne' := L_bot},
   have meas_Ec : μ Eᶜ = 1 - μ E,
   { simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne, },
@@ -1094,7 +1094,7 @@ lemma limsup_measure_compl_le_of_le_liminf_measure
 begin
   by_cases L_bot : L = ⊥,
   { simp only [L_bot, bot_le,
-      (show limsup ⊥ (λ i, μs i Eᶜ) = ⊥, by simp only [limsup, filter.map_bot, Limsup_bot])], },
+      (show limsup (λ i, μs i Eᶜ) ⊥ = ⊥, by simp only [limsup, filter.map_bot, Limsup_bot])], },
   haveI : L.ne_bot, from {ne' := L_bot},
   have meas_Ec : μ Eᶜ = 1 - μ E,
   { simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne, },
diff --git a/src/measure_theory/measure/hausdorff.lean b/src/measure_theory/measure/hausdorff.lean
index fb4aa3800f7ec..da0be5b93bb46 100644
--- a/src/measure_theory/measure/hausdorff.lean
+++ b/src/measure_theory/measure/hausdorff.lean
@@ -514,7 +514,7 @@ lemma mk_metric_le_liminf_tsum {β : Type*} {ι : β → Type*} [∀ n, countabl
   {l : filter β} (r : β → ℝ≥0∞) (hr : tendsto r l (𝓝 0)) (t : Π (n : β), ι n → set X)
   (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i)
   (m : ℝ≥0∞ → ℝ≥0∞) :
-  mk_metric m s ≤ liminf l (λ n, ∑' i, m (diam (t n i))) :=
+  mk_metric m s ≤ liminf (λ n, ∑' i, m (diam (t n i))) l :=
 begin
   haveI : Π n, encodable (ι n) := λ n, encodable.of_countable _,
   simp only [mk_metric_apply],
@@ -541,7 +541,7 @@ lemma mk_metric_le_liminf_sum {β : Type*} {ι : β → Type*} [hι : ∀ n, fin
   {l : filter β} (r : β → ℝ≥0∞) (hr : tendsto r l (𝓝 0)) (t : Π (n : β), ι n → set X)
   (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i)
   (m : ℝ≥0∞ → ℝ≥0∞) :
-  mk_metric m s ≤ liminf l (λ n, ∑ i, m (diam (t n i))) :=
+  mk_metric m s ≤ liminf (λ n, ∑ i, m (diam (t n i))) l :=
 by simpa only [tsum_fintype] using mk_metric_le_liminf_tsum s r hr t ht hst m
 
 /-!
@@ -571,7 +571,7 @@ lemma hausdorff_measure_le_liminf_tsum {β : Type*}  {ι : β → Type*} [hι :
   (d : ℝ) (s : set X)
   {l : filter β} (r : β → ℝ≥0∞) (hr : tendsto r l (𝓝 0)) (t : Π (n : β), ι n → set X)
   (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) :
-  μH[d] s ≤ liminf l (λ n, ∑' i, diam (t n i) ^ d) :=
+  μH[d] s ≤ liminf (λ n, ∑' i, diam (t n i) ^ d) l :=
 mk_metric_le_liminf_tsum s r hr t ht hst _
 
 /-- To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending
@@ -580,7 +580,7 @@ lemma hausdorff_measure_le_liminf_sum {β : Type*}  {ι : β → Type*} [hι : 
   (d : ℝ) (s : set X)
   {l : filter β} (r : β → ℝ≥0∞) (hr : tendsto r l (𝓝 0)) (t : Π (n : β), ι n → set X)
   (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) :
-  μH[d] s ≤ liminf l (λ n, ∑ i, diam (t n i) ^ d) :=
+  μH[d] s ≤ liminf (λ n, ∑ i, diam (t n i) ^ d) l :=
 mk_metric_le_liminf_sum s r hr t ht hst _
 
 /-- If `d₁ < d₂`, then for any set `s` we have either `μH[d₂] s = 0`, or `μH[d₁] s = ∞`. -/
@@ -753,10 +753,10 @@ begin
       ... ≤ (a i : ℝ) + (⌊(x i - a i) * n⌋₊ + 1) / n :
         add_le_add le_rfl ((div_le_div_right npos).2 (nat.lt_floor_add_one _).le) } },
   calc μH[fintype.card ι] (set.pi univ (λ (i : ι), Ioo (a i : ℝ) (b i)))
-    ≤ liminf at_top (λ (n : ℕ), ∑ (i : γ n), diam (t n i) ^ ↑(fintype.card ι)) :
+    ≤ liminf (λ (n : ℕ), ∑ (i : γ n), diam (t n i) ^ ↑(fintype.card ι)) at_top :
       hausdorff_measure_le_liminf_sum _ (set.pi univ (λ i, Ioo (a i : ℝ) (b i)))
         (λ (n : ℕ), 1/(n : ℝ≥0∞)) A t B C
-  ... ≤ liminf at_top (λ (n : ℕ), ∑ (i : γ n), (1/n) ^ (fintype.card ι)) :
+  ... ≤ liminf (λ (n : ℕ), ∑ (i : γ n), (1/n) ^ (fintype.card ι)) at_top :
     begin
       refine liminf_le_liminf _ (by is_bounded_default),
       filter_upwards [B] with _ hn,
@@ -764,7 +764,7 @@ begin
       rw ennreal.rpow_nat_cast,
       exact pow_le_pow_of_le_left' (hn i) _,
     end
-  ... = liminf at_top (λ (n : ℕ), ∏ (i : ι), (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) :
+  ... = liminf (λ (n : ℕ), ∏ (i : ι), (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) at_top :
   begin
     simp only [finset.card_univ, nat.cast_prod, one_mul, fintype.card_fin,
       finset.sum_const, nsmul_eq_mul, fintype.card_pi, div_eq_mul_inv, finset.prod_mul_distrib,
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
index eaf74338f9bc9..3b978df81e1fd 100644
--- a/src/measure_theory/measure/measure_space.lean
+++ b/src/measure_theory/measure/measure_space.lean
@@ -503,13 +503,13 @@ end
 
 /-- One direction of the **Borel-Cantelli lemma**: if (sᵢ) is a sequence of sets such
 that `∑ μ sᵢ` is finite, then the limit superior of the `sᵢ` is a null set. -/
-lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∑' i, μ (s i) ≠ ∞) : μ (limsup at_top s) = 0 :=
+lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∑' i, μ (s i) ≠ ∞) : μ (limsup s at_top) = 0 :=
 begin
   -- First we replace the sequence `sₙ` with a sequence of measurable sets `tₙ ⊇ sₙ` of the same
   -- measure.
   set t : ℕ → set α := λ n, to_measurable μ (s n),
   have ht : ∑' i, μ (t i) ≠ ∞, by simpa only [t, measure_to_measurable] using hs,
-  suffices : μ (limsup at_top t) = 0,
+  suffices : μ (limsup t at_top) = 0,
   { have A : s ≤ t := λ n, subset_to_measurable μ (s n),
     -- TODO default args fail
     exact measure_mono_null (limsup_le_limsup (eventually_of_forall (pi.le_def.mp A))
diff --git a/src/order/liminf_limsup.lean b/src/order/liminf_limsup.lean
index d6caaef0e8ee0..279f595ef96de 100644
--- a/src/order/liminf_limsup.lean
+++ b/src/order/liminf_limsup.lean
@@ -11,9 +11,9 @@ import order.filter.cofinite
 Defines the Liminf/Limsup of a function taking values in a conditionally complete lattice, with
 respect to an arbitrary filter.
 
-We define `f.Limsup` (`f.Liminf`) where `f` is a filter taking values in a conditionally complete
-lattice. `f.Limsup` is the smallest element `a` such that, eventually, `u ≤ a` (and vice versa for
-`f.Liminf`). To work with the Limsup along a function `u` use `(f.map u).Limsup`.
+We define `Limsup f` (`Liminf f`) where `f` is a filter taking values in a conditionally complete
+lattice. `Limsup f` is the smallest element `a` such that, eventually, `u ≤ a` (and vice versa for
+`Liminf f`). To work with the Limsup along a function `u` use `Limsup (map u f)`.
 
 Usually, one defines the Limsup as `Inf (Sup s)` where the Inf is taken over all sets in the filter.
 For instance, in ℕ along a function `u`, this is `Inf_n (Sup_{k ≥ n} u k)` (and the latter quantity
@@ -48,7 +48,7 @@ def is_bounded (r : α → α → Prop) (f : filter α) := ∃ b, ∀ᶠ x in f,
 
 /-- `f.is_bounded_under (≺) u`: the image of the filter `f` under `u` is eventually bounded w.r.t.
 the relation `≺`, i.e. eventually, it is bounded by some uniform bound. -/
-def is_bounded_under (r : α → α → Prop) (f : filter β) (u : β → α) := (f.map u).is_bounded r
+def is_bounded_under (r : α → α → Prop) (f : filter β) (u : β → α) := (map u f).is_bounded r
 
 variables {r : α → α → Prop} {f g : filter α}
 
@@ -154,7 +154,7 @@ def is_cobounded (r : α → α → Prop) (f : filter α) := ∃b, ∀a, (∀ᶠ
 /-- `is_cobounded_under (≺) f u` states that the image of the filter `f` under the map `u` does not
 tend to infinity w.r.t. `≺`. This is also called frequently bounded. Will be usually instantiated
 with `≤` or `≥`. -/
-def is_cobounded_under (r : α → α → Prop) (f : filter β) (u : β → α) := (f.map u).is_cobounded r
+def is_cobounded_under (r : α → α → Prop) (f : filter β) (u : β → α) := (map u f).is_cobounded r
 
 /-- To check that a filter is frequently bounded, it suffices to have a witness
 which bounds `f` at some point for every admissible set.
@@ -273,124 +273,165 @@ def Liminf (f : filter α) : α := Sup { a | ∀ᶠ n in f, a ≤ n }
 
 /-- The `limsup` of a function `u` along a filter `f` is the infimum of the `a` such that,
 eventually for `f`, holds `u x ≤ a`. -/
-def limsup (f : filter β) (u : β → α) : α := (f.map u).Limsup
+def limsup (u : β → α) (f : filter β) : α := Limsup (map u f)
 
 /-- The `liminf` of a function `u` along a filter `f` is the supremum of the `a` such that,
 eventually for `f`, holds `u x ≥ a`. -/
-def liminf (f : filter β) (u : β → α) : α := (f.map u).Liminf
+def liminf (u : β → α) (f : filter β) : α := Liminf (map u f)
+
+/-- The `blimsup` of a function `u` along a filter `f`, bounded by a predicate `p`, is the infimum
+of the `a` such that, eventually for `f`, `u x ≤ a` whenever `p x` holds. -/
+def blimsup (u : β → α) (f : filter β) (p : β → Prop) :=
+Inf { a | ∀ᶠ x in f, p x → u x ≤ a }
+
+/-- The `bliminf` of a function `u` along a filter `f`, bounded by a predicate `p`, is the supremum
+of the `a` such that, eventually for `f`, `a ≤ u x` whenever `p x` holds. -/
+def bliminf (u : β → α) (f : filter β) (p : β → Prop) :=
+Sup { a | ∀ᶠ x in f, p x → a ≤ u x }
 
 section
-variables {f : filter β} {u : β → α}
-theorem limsup_eq : f.limsup u = Inf { a | ∀ᶠ n in f, u n ≤ a } := rfl
-theorem liminf_eq : f.liminf u = Sup { a | ∀ᶠ n in f, a ≤ u n } := rfl
+
+variables {f : filter β} {u : β → α} {p : β → Prop}
+
+theorem limsup_eq : limsup u f = Inf { a | ∀ᶠ n in f, u n ≤ a } := rfl
+
+theorem liminf_eq : liminf u f = Sup { a | ∀ᶠ n in f, a ≤ u n } := rfl
+
+theorem blimsup_eq : blimsup u f p = Inf { a | ∀ᶠ x in f, p x → u x ≤ a } := rfl
+
+theorem bliminf_eq : bliminf u f p = Sup { a | ∀ᶠ x in f, p x → a ≤ u x } := rfl
+
+end
+
+@[simp] lemma blimsup_true (f : filter β) (u : β → α) :
+  blimsup u f (λ x, true) = limsup u f :=
+by simp [blimsup_eq, limsup_eq]
+
+@[simp] lemma bliminf_true (f : filter β) (u : β → α) :
+  bliminf u f (λ x, true) = liminf u f :=
+by simp [bliminf_eq, liminf_eq]
+
+lemma blimsup_eq_limsup_subtype {f : filter β} {u : β → α} {p : β → Prop} :
+  blimsup u f p = limsup (u ∘ (coe : {x | p x} → β)) (comap coe f) :=
+begin
+  simp only [blimsup_eq, limsup_eq, function.comp_app, eventually_comap, set_coe.forall,
+    subtype.coe_mk, mem_set_of_eq],
+  congr,
+  ext a,
+  exact eventually_congr (eventually_of_forall
+    (λ x, ⟨λ hx y hy hxy, hxy.symm ▸ (hx (hxy ▸ hy)), λ hx hx', hx x hx' rfl⟩)),
 end
 
+lemma bliminf_eq_liminf_subtype {f : filter β} {u : β → α} {p : β → Prop} :
+  bliminf u f p = liminf (u ∘ (coe : {x | p x} → β)) (comap coe f) :=
+@blimsup_eq_limsup_subtype αᵒᵈ β _ f u p
+
 theorem Limsup_le_of_le {f : filter α} {a}
-  (hf : f.is_cobounded (≤) . is_bounded_default) (h : ∀ᶠ n in f, n ≤ a) : f.Limsup ≤ a :=
+  (hf : f.is_cobounded (≤) . is_bounded_default) (h : ∀ᶠ n in f, n ≤ a) : Limsup f ≤ a :=
 cInf_le hf h
 
 theorem le_Liminf_of_le {f : filter α} {a}
-  (hf : f.is_cobounded (≥) . is_bounded_default) (h : ∀ᶠ n in f, a ≤ n) : a ≤ f.Liminf :=
+  (hf : f.is_cobounded (≥) . is_bounded_default) (h : ∀ᶠ n in f, a ≤ n) : a ≤ Liminf f :=
 le_cSup hf h
 
 theorem limsup_le_of_le {f : filter β} {u : β → α} {a}
   (hf : f.is_cobounded_under (≤) u . is_bounded_default) (h : ∀ᶠ n in f, u n ≤ a) :
-  f.limsup u ≤ a :=
+  limsup u f ≤ a :=
 cInf_le hf h
 
 theorem le_liminf_of_le {f : filter β} {u : β → α} {a}
   (hf : f.is_cobounded_under (≥) u . is_bounded_default) (h : ∀ᶠ n in f, a ≤ u n) :
-    a ≤ f.liminf u :=
+    a ≤ liminf u f :=
 le_cSup hf h
 
 theorem le_Limsup_of_le {f : filter α} {a}
   (hf : f.is_bounded (≤) . is_bounded_default) (h : ∀ b, (∀ᶠ n in f, n ≤ b) → a ≤ b) :
-  a ≤ f.Limsup :=
+  a ≤ Limsup f :=
 le_cInf hf h
 
 theorem Liminf_le_of_le {f : filter α} {a}
   (hf : f.is_bounded (≥) . is_bounded_default) (h : ∀ b, (∀ᶠ n in f, b ≤ n) → b ≤ a) :
-  f.Liminf ≤ a :=
+  Liminf f ≤ a :=
 cSup_le hf h
 
 theorem le_limsup_of_le {f : filter β} {u : β → α} {a}
   (hf : f.is_bounded_under (≤) u . is_bounded_default) (h : ∀ b, (∀ᶠ n in f, u n ≤ b) → a ≤ b) :
-  a ≤ f.limsup u :=
+  a ≤ limsup u f :=
 le_cInf hf h
 
 theorem liminf_le_of_le {f : filter β} {u : β → α} {a}
   (hf : f.is_bounded_under (≥) u . is_bounded_default) (h : ∀ b, (∀ᶠ n in f, b ≤ u n) → b ≤ a) :
-  f.liminf u ≤ a :=
+  liminf u f ≤ a :=
 cSup_le hf h
 
 theorem Liminf_le_Limsup {f : filter α} [ne_bot f]
   (h₁ : f.is_bounded (≤) . is_bounded_default) (h₂ : f.is_bounded (≥) . is_bounded_default) :
-  f.Liminf ≤ f.Limsup :=
+  Liminf f ≤ Limsup f :=
 Liminf_le_of_le h₂ $ assume a₀ ha₀, le_Limsup_of_le h₁ $ assume a₁ ha₁,
   show a₀ ≤ a₁, from let ⟨b, hb₀, hb₁⟩ := (ha₀.and ha₁).exists in le_trans hb₀ hb₁
 
 lemma liminf_le_limsup {f : filter β} [ne_bot f] {u : β → α}
   (h : f.is_bounded_under (≤) u . is_bounded_default)
   (h' : f.is_bounded_under (≥) u . is_bounded_default) :
-  liminf f u ≤ limsup f u :=
+  liminf u f ≤ limsup u f :=
 Liminf_le_Limsup h h'
 
 lemma Limsup_le_Limsup {f g : filter α}
   (hf : f.is_cobounded (≤) . is_bounded_default) (hg : g.is_bounded (≤) . is_bounded_default)
-  (h : ∀ a, (∀ᶠ n in g, n ≤ a) → ∀ᶠ n in f, n ≤ a) : f.Limsup ≤ g.Limsup :=
+  (h : ∀ a, (∀ᶠ n in g, n ≤ a) → ∀ᶠ n in f, n ≤ a) : Limsup f ≤ Limsup g :=
 cInf_le_cInf hf hg h
 
 lemma Liminf_le_Liminf {f g : filter α}
   (hf : f.is_bounded (≥) . is_bounded_default) (hg : g.is_cobounded (≥) . is_bounded_default)
-  (h : ∀ a, (∀ᶠ n in f, a ≤ n) → ∀ᶠ n in g, a ≤ n) : f.Liminf ≤ g.Liminf :=
+  (h : ∀ a, (∀ᶠ n in f, a ≤ n) → ∀ᶠ n in g, a ≤ n) : Liminf f ≤ Liminf g :=
 cSup_le_cSup hg hf h
 
 lemma limsup_le_limsup {α : Type*} [conditionally_complete_lattice β] {f : filter α} {u v : α → β}
   (h : u ≤ᶠ[f] v)
   (hu : f.is_cobounded_under (≤) u . is_bounded_default)
   (hv : f.is_bounded_under (≤) v . is_bounded_default) :
-  f.limsup u ≤ f.limsup v :=
+  limsup u f ≤ limsup v f :=
 Limsup_le_Limsup hu hv $ assume b, h.trans
 
 lemma liminf_le_liminf {α : Type*} [conditionally_complete_lattice β] {f : filter α} {u v : α → β}
   (h : ∀ᶠ a in f, u a ≤ v a)
   (hu : f.is_bounded_under (≥) u . is_bounded_default)
   (hv : f.is_cobounded_under (≥) v . is_bounded_default) :
-  f.liminf u ≤ f.liminf v :=
+  liminf u f ≤ liminf v f :=
 @limsup_le_limsup βᵒᵈ α _ _ _ _ h hv hu
 
 lemma Limsup_le_Limsup_of_le {f g : filter α} (h : f ≤ g)
   (hf : f.is_cobounded (≤) . is_bounded_default) (hg : g.is_bounded (≤) . is_bounded_default) :
-  f.Limsup ≤ g.Limsup :=
+  Limsup f ≤ Limsup g :=
 Limsup_le_Limsup hf hg (assume a ha, h ha)
 
 lemma Liminf_le_Liminf_of_le {f g : filter α} (h : g ≤ f)
   (hf : f.is_bounded (≥) . is_bounded_default) (hg : g.is_cobounded (≥) . is_bounded_default) :
-  f.Liminf ≤ g.Liminf :=
+  Liminf f ≤ Liminf g :=
 Liminf_le_Liminf hf hg (assume a ha, h ha)
 
 lemma limsup_le_limsup_of_le {α β} [conditionally_complete_lattice β] {f g : filter α} (h : f ≤ g)
   {u : α → β} (hf : f.is_cobounded_under (≤) u . is_bounded_default)
   (hg : g.is_bounded_under (≤) u . is_bounded_default) :
-  f.limsup u ≤ g.limsup u :=
+  limsup u f ≤ limsup u g :=
 Limsup_le_Limsup_of_le (map_mono h) hf hg
 
 lemma liminf_le_liminf_of_le {α β} [conditionally_complete_lattice β] {f g : filter α} (h : g ≤ f)
   {u : α → β} (hf : f.is_bounded_under (≥) u . is_bounded_default)
   (hg : g.is_cobounded_under (≥) u . is_bounded_default) :
-  f.liminf u ≤ g.liminf u :=
+  liminf u f ≤ liminf u g :=
 Liminf_le_Liminf_of_le (map_mono h) hf hg
 
 theorem Limsup_principal {s : set α} (h : bdd_above s) (hs : s.nonempty) :
-  (𝓟 s).Limsup = Sup s :=
+  Limsup (𝓟 s) = Sup s :=
 by simp [Limsup]; exact cInf_upper_bounds_eq_cSup h hs
 
 theorem Liminf_principal {s : set α} (h : bdd_below s) (hs : s.nonempty) :
-  (𝓟 s).Liminf = Inf s :=
+  Liminf (𝓟 s) = Inf s :=
 @Limsup_principal αᵒᵈ _ s h hs
 
 lemma limsup_congr {α : Type*} [conditionally_complete_lattice β] {f : filter α} {u v : α → β}
-  (h : ∀ᶠ a in f, u a = v a) : limsup f u = limsup f v :=
+  (h : ∀ᶠ a in f, u a = v a) : limsup u f = limsup v f :=
 begin
   rw limsup_eq,
   congr' with b,
@@ -398,15 +439,15 @@ begin
 end
 
 lemma liminf_congr {α : Type*} [conditionally_complete_lattice β] {f : filter α} {u v : α → β}
-  (h : ∀ᶠ a in f, u a = v a) : liminf f u = liminf f v :=
+  (h : ∀ᶠ a in f, u a = v a) : liminf u f = liminf v f :=
 @limsup_congr βᵒᵈ _ _ _ _ _ h
 
 lemma limsup_const {α : Type*} [conditionally_complete_lattice β] {f : filter α} [ne_bot f]
-  (b : β) : limsup f (λ x, b) = b :=
+  (b : β) : limsup (λ x, b) f = b :=
 by simpa only [limsup_eq, eventually_const] using cInf_Ici
 
 lemma liminf_const {α : Type*} [conditionally_complete_lattice β] {f : filter α} [ne_bot f]
-  (b : β) : liminf f (λ x, b) = b :=
+  (b : β) : liminf (λ x, b) f = b :=
 @limsup_const βᵒᵈ α _ f _ b
 
 
@@ -415,88 +456,114 @@ end conditionally_complete_lattice
 section complete_lattice
 variables [complete_lattice α]
 
-@[simp] theorem Limsup_bot : (⊥ : filter α).Limsup = ⊥ :=
+@[simp] theorem Limsup_bot : Limsup (⊥ : filter α) = ⊥ :=
 bot_unique $ Inf_le $ by simp
 
-@[simp] theorem Liminf_bot : (⊥ : filter α).Liminf = ⊤ :=
+@[simp] theorem Liminf_bot : Liminf (⊥ : filter α) = ⊤ :=
 top_unique $ le_Sup $ by simp
 
-@[simp] theorem Limsup_top : (⊤ : filter α).Limsup = ⊤ :=
+@[simp] theorem Limsup_top : Limsup (⊤ : filter α) = ⊤ :=
 top_unique $ le_Inf $
   by simp [eq_univ_iff_forall]; exact assume b hb, (top_unique $ hb _)
 
-@[simp] theorem Liminf_top : (⊤ : filter α).Liminf = ⊥ :=
+@[simp] theorem Liminf_top : Liminf (⊤ : filter α) = ⊥ :=
 bot_unique $ Sup_le $
   by simp [eq_univ_iff_forall]; exact assume b hb, (bot_unique $ hb _)
 
+@[simp] lemma blimsup_false {f : filter β} {u : β → α} :
+  blimsup u f (λ x, false) = ⊥ :=
+by simp [blimsup_eq]
+
+@[simp] lemma bliminf_false {f : filter β} {u : β → α} :
+  bliminf u f (λ x, false) = ⊤ :=
+by simp [bliminf_eq]
+
 /-- Same as limsup_const applied to `⊥` but without the `ne_bot f` assumption -/
-lemma limsup_const_bot {f : filter β} : limsup f (λ x : β, (⊥ : α)) = (⊥ : α) :=
+lemma limsup_const_bot {f : filter β} : limsup (λ x : β, (⊥ : α)) f = (⊥ : α) :=
 begin
   rw [limsup_eq, eq_bot_iff],
   exact Inf_le (eventually_of_forall (λ x, le_rfl)),
 end
 
 /-- Same as limsup_const applied to `⊤` but without the `ne_bot f` assumption -/
-lemma liminf_const_top {f : filter β} : liminf f (λ x : β, (⊤ : α)) = (⊤ : α) :=
+lemma liminf_const_top {f : filter β} : liminf (λ x : β, (⊤ : α)) f = (⊤ : α) :=
 @limsup_const_bot αᵒᵈ β _ _
 
 theorem has_basis.Limsup_eq_infi_Sup {ι} {p : ι → Prop} {s} {f : filter α} (h : f.has_basis p s) :
-  f.Limsup = ⨅ i (hi : p i), Sup (s i) :=
+  Limsup f = ⨅ i (hi : p i), Sup (s i) :=
 le_antisymm
   (le_infi₂ $ λ i hi, Inf_le $ h.eventually_iff.2 ⟨i, hi, λ x, le_Sup⟩)
   (le_Inf $ assume a ha, let ⟨i, hi, ha⟩ := h.eventually_iff.1 ha in
     infi₂_le_of_le _ hi $ Sup_le ha)
 
 theorem has_basis.Liminf_eq_supr_Inf {p : ι → Prop} {s : ι → set α} {f : filter α}
-  (h : f.has_basis p s) : f.Liminf = ⨆ i (hi : p i), Inf (s i) :=
+  (h : f.has_basis p s) : Liminf f = ⨆ i (hi : p i), Inf (s i) :=
 @has_basis.Limsup_eq_infi_Sup αᵒᵈ _ _ _ _ _ h
 
-theorem Limsup_eq_infi_Sup {f : filter α} : f.Limsup = ⨅ s ∈ f, Sup s :=
+theorem Limsup_eq_infi_Sup {f : filter α} : Limsup f = ⨅ s ∈ f, Sup s :=
 f.basis_sets.Limsup_eq_infi_Sup
 
-theorem Liminf_eq_supr_Inf {f : filter α} : f.Liminf = ⨆ s ∈ f, Inf s :=
+theorem Liminf_eq_supr_Inf {f : filter α} : Liminf f = ⨆ s ∈ f, Inf s :=
 @Limsup_eq_infi_Sup αᵒᵈ _ _
 
-theorem limsup_le_supr {f : filter β} {u : β → α} : f.limsup u ≤ ⨆ n, u n :=
+theorem limsup_le_supr {f : filter β} {u : β → α} : limsup u f ≤ ⨆ n, u n :=
 limsup_le_of_le (by is_bounded_default) (eventually_of_forall (le_supr u))
 
-theorem infi_le_liminf {f : filter β} {u : β → α} : (⨅ n, u n) ≤ f.liminf u :=
+theorem infi_le_liminf {f : filter β} {u : β → α} : (⨅ n, u n) ≤ liminf u f :=
 le_liminf_of_le (by is_bounded_default) (eventually_of_forall (infi_le u))
 
 /-- In a complete lattice, the limsup of a function is the infimum over sets `s` in the filter
 of the supremum of the function over `s` -/
-theorem limsup_eq_infi_supr {f : filter β} {u : β → α} : f.limsup u = ⨅ s ∈ f, ⨆ a ∈ s, u a :=
+theorem limsup_eq_infi_supr {f : filter β} {u : β → α} : limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a :=
 (f.basis_sets.map u).Limsup_eq_infi_Sup.trans $
   by simp only [Sup_image, id]
 
-lemma limsup_eq_infi_supr_of_nat {u : ℕ → α} : limsup at_top u = ⨅ n : ℕ, ⨆ i ≥ n, u i :=
+lemma limsup_eq_infi_supr_of_nat {u : ℕ → α} : limsup u at_top = ⨅ n : ℕ, ⨆ i ≥ n, u i :=
 (at_top_basis.map u).Limsup_eq_infi_Sup.trans $
   by simp only [Sup_image, infi_const]; refl
 
-lemma limsup_eq_infi_supr_of_nat' {u : ℕ → α} : limsup at_top u = ⨅ n : ℕ, ⨆ i : ℕ, u (i + n) :=
+lemma limsup_eq_infi_supr_of_nat' {u : ℕ → α} : limsup u at_top = ⨅ n : ℕ, ⨆ i : ℕ, u (i + n) :=
 by simp only [limsup_eq_infi_supr_of_nat, supr_ge_eq_supr_nat_add]
 
 theorem has_basis.limsup_eq_infi_supr {p : ι → Prop} {s : ι → set β} {f : filter β} {u : β → α}
-  (h : f.has_basis p s) : f.limsup u = ⨅ i (hi : p i), ⨆ a ∈ s i, u a :=
+  (h : f.has_basis p s) : limsup u f = ⨅ i (hi : p i), ⨆ a ∈ s i, u a :=
 (h.map u).Limsup_eq_infi_Sup.trans $ by simp only [Sup_image, id]
 
+lemma blimsup_eq_infi_bsupr {f : filter β} {p : β → Prop} {u : β → α} :
+  blimsup u f p = ⨅ s ∈ f, ⨆ b (hb : p b ∧ b ∈ s), u b :=
+begin
+  refine le_antisymm (Inf_le_Inf _) (infi_le_iff.mpr $ λ a ha, le_Inf_iff.mpr $ λ a' ha', _),
+  { rintros - ⟨s, rfl⟩,
+    simp only [mem_set_of_eq, le_infi_iff],
+    conv { congr, funext, rw imp.swap, },
+    refine eventually_imp_distrib_left.mpr (λ h, eventually_iff_exists_mem.2 ⟨s, h, λ x h₁ h₂, _⟩),
+    exact @le_supr₂ α β (λ b, p b ∧ b ∈ s) _ (λ b hb, u b) x ⟨h₂, h₁⟩, },
+  { obtain ⟨s, hs, hs'⟩ := eventually_iff_exists_mem.mp ha',
+    simp_rw imp.swap at hs',
+    exact (le_infi_iff.mp (ha s) hs).trans (by simpa only [supr₂_le_iff, and_imp]), },
+end
+
 /-- In a complete lattice, the liminf of a function is the infimum over sets `s` in the filter
 of the supremum of the function over `s` -/
-theorem liminf_eq_supr_infi {f : filter β} {u : β → α} : f.liminf u = ⨆ s ∈ f, ⨅ a ∈ s, u a :=
+theorem liminf_eq_supr_infi {f : filter β} {u : β → α} : liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a :=
 @limsup_eq_infi_supr αᵒᵈ β _ _ _
 
-lemma liminf_eq_supr_infi_of_nat {u : ℕ → α} : liminf at_top u = ⨆ n : ℕ, ⨅ i ≥ n, u i :=
+lemma liminf_eq_supr_infi_of_nat {u : ℕ → α} : liminf u at_top = ⨆ n : ℕ, ⨅ i ≥ n, u i :=
 @limsup_eq_infi_supr_of_nat αᵒᵈ _ u
 
-lemma liminf_eq_supr_infi_of_nat' {u : ℕ → α} : liminf at_top u = ⨆ n : ℕ, ⨅ i : ℕ, u (i + n) :=
+lemma liminf_eq_supr_infi_of_nat' {u : ℕ → α} : liminf u at_top = ⨆ n : ℕ, ⨅ i : ℕ, u (i + n) :=
 @limsup_eq_infi_supr_of_nat' αᵒᵈ _ _
 
 theorem has_basis.liminf_eq_supr_infi {p : ι → Prop} {s : ι → set β} {f : filter β} {u : β → α}
-  (h : f.has_basis p s) : f.liminf u = ⨆ i (hi : p i), ⨅ a ∈ s i, u a :=
+  (h : f.has_basis p s) : liminf u f = ⨆ i (hi : p i), ⨅ a ∈ s i, u a :=
 @has_basis.limsup_eq_infi_supr αᵒᵈ _ _ _ _ _ _ _ h
 
+lemma bliminf_eq_supr_binfi {f : filter β} {p : β → Prop} {u : β → α} :
+  bliminf u f p = ⨆ s ∈ f, ⨅ b (hb : p b ∧ b ∈ s), u b :=
+@blimsup_eq_infi_bsupr αᵒᵈ β _ f p u
+
 lemma limsup_eq_Inf_Sup {ι R : Type*} (F : filter ι) [complete_lattice R] (a : ι → R) :
-  F.limsup a = Inf ((λ I, Sup (a '' I)) '' F.sets) :=
+  limsup a F = Inf ((λ I, Sup (a '' I)) '' F.sets) :=
 begin
   refine le_antisymm _ _,
   { rw limsup_eq,
@@ -511,20 +578,20 @@ begin
 end
 
 lemma liminf_eq_Sup_Inf {ι R : Type*} (F : filter ι) [complete_lattice R] (a : ι → R) :
-  F.liminf a = Sup ((λ I, Inf (a '' I)) '' F.sets) :=
+  liminf a F = Sup ((λ I, Inf (a '' I)) '' F.sets) :=
 @filter.limsup_eq_Inf_Sup ι (order_dual R) _ _ a
 
 @[simp] lemma liminf_nat_add (f : ℕ → α) (k : ℕ) :
-  at_top.liminf (λ i, f (i + k)) = at_top.liminf f :=
+  liminf (λ i, f (i + k)) at_top = liminf f at_top :=
 by { simp_rw liminf_eq_supr_infi_of_nat, exact supr_infi_ge_nat_add f k }
 
 @[simp] lemma limsup_nat_add (f : ℕ → α) (k : ℕ) :
-  at_top.limsup (λ i, f (i + k)) = at_top.limsup f :=
+  limsup (λ i, f (i + k)) at_top = limsup f at_top :=
 @liminf_nat_add αᵒᵈ _ f k
 
 lemma liminf_le_of_frequently_le' {α β} [complete_lattice β]
   {f : filter α} {u : α → β} {x : β} (h : ∃ᶠ a in f, u a ≤ x) :
-  f.liminf u ≤ x :=
+  liminf u f ≤ x :=
 begin
   rw liminf_eq,
   refine Sup_le (λ b hb, _),
@@ -537,15 +604,124 @@ end
 
 lemma le_limsup_of_frequently_le' {α β} [complete_lattice β]
   {f : filter α} {u : α → β} {x : β} (h : ∃ᶠ a in f, x ≤ u a) :
-  x ≤ f.limsup u :=
+  x ≤ limsup u f :=
 @liminf_le_of_frequently_le' _ βᵒᵈ _ _ _ _ h
 
+variables {f g : filter β} {p q : β → Prop} {u v : β → α}
+
+lemma blimsup_mono (h : ∀ x, p x → q x) :
+  blimsup u f p ≤ blimsup u f q :=
+Inf_le_Inf $ λ a ha, ha.mono $ by tauto
+
+lemma bliminf_antitone (h : ∀ x, p x → q x) :
+  bliminf u f q ≤ bliminf u f p :=
+Sup_le_Sup $ λ a ha, ha.mono $ by tauto
+
+lemma mono_blimsup' (h : ∀ᶠ x in f, u x ≤ v x) :
+  blimsup u f p ≤ blimsup v f p :=
+Inf_le_Inf $ λ a ha, (ha.and h).mono $ λ x hx hx', hx.2.trans (hx.1 hx')
+
+lemma mono_blimsup (h : ∀ x, u x ≤ v x) :
+  blimsup u f p ≤ blimsup v f p :=
+mono_blimsup' $ eventually_of_forall h
+
+lemma mono_bliminf' (h : ∀ᶠ x in f, u x ≤ v x) :
+  bliminf u f p ≤ bliminf v f p :=
+Sup_le_Sup $ λ a ha, (ha.and h).mono $ λ x hx hx', (hx.1 hx').trans hx.2
+
+lemma mono_bliminf (h : ∀ x, u x ≤ v x) :
+  bliminf u f p ≤ bliminf v f p :=
+mono_bliminf' $ eventually_of_forall h
+
+lemma bliminf_antitone_filter (h : f ≤ g) :
+  bliminf u g p ≤ bliminf u f p :=
+Sup_le_Sup $ λ a ha, ha.filter_mono h
+
+lemma blimsup_monotone_filter (h : f ≤ g) :
+  blimsup u f p ≤ blimsup u g p :=
+Inf_le_Inf $ λ a ha, ha.filter_mono h
+
+@[simp] lemma blimsup_and_le_inf :
+  blimsup u f (λ x, p x ∧ q x) ≤ blimsup u f p ⊓ blimsup u f q :=
+le_inf (blimsup_mono $ by tauto) (blimsup_mono $ by tauto)
+
+@[simp] lemma bliminf_sup_le_and :
+  bliminf u f p ⊔ bliminf u f q ≤ bliminf u f (λ x, p x ∧ q x) :=
+@blimsup_and_le_inf αᵒᵈ β _ f p q u
+
+/-- See also `filter.blimsup_or_eq_sup`. -/
+@[simp] lemma blimsup_sup_le_or :
+  blimsup u f p ⊔ blimsup u f q ≤ blimsup u f (λ x, p x ∨ q x) :=
+sup_le (blimsup_mono $ by tauto) (blimsup_mono $ by tauto)
+
+/-- See also `filter.bliminf_or_eq_inf`. -/
+@[simp] lemma bliminf_or_le_inf :
+  bliminf u f (λ x, p x ∨ q x) ≤ bliminf u f p ⊓ bliminf u f q :=
+@blimsup_sup_le_or αᵒᵈ β _ f p q u
+
 end complete_lattice
 
+section complete_distrib_lattice
+
+variables [complete_distrib_lattice α] {f : filter β} {p q : β → Prop} {u : β → α}
+
+@[simp] lemma blimsup_or_eq_sup :
+  blimsup u f (λ x, p x ∨ q x) = blimsup u f p ⊔ blimsup u f q :=
+begin
+  refine le_antisymm _ blimsup_sup_le_or,
+  simp only [blimsup_eq, Inf_sup_eq, sup_Inf_eq, le_infi₂_iff, mem_set_of_eq],
+  refine λ a' ha' a ha, Inf_le ((ha.and ha').mono $ λ b h hb, _),
+  exact or.elim hb (λ hb, le_sup_of_le_left $ h.1 hb) (λ hb, le_sup_of_le_right $ h.2 hb),
+end
+
+@[simp] lemma bliminf_or_eq_inf :
+  bliminf u f (λ x, p x ∨ q x) = bliminf u f p ⊓ bliminf u f q :=
+@blimsup_or_eq_sup αᵒᵈ β _ f p q u
+
+end complete_distrib_lattice
+
+section set_lattice
+
+variables {p : ι → Prop} {s : ι → set α}
+
+lemma cofinite.blimsup_set_eq :
+  blimsup s cofinite p = { x | { n | p n ∧ x ∈ s n }.infinite } :=
+begin
+  simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, Inf_eq_sInter, exists_prop],
+  ext x,
+  refine ⟨λ h, _, λ hx t h, _⟩;
+  contrapose! h,
+  { simp only [mem_sInter, mem_set_of_eq, not_forall, exists_prop],
+    exact ⟨{x}ᶜ, by simpa using h, by simp⟩, },
+  { exact hx.mono (λ i hi, ⟨hi.1, λ hit, h (hit hi.2)⟩), },
+end
+
+lemma cofinite.bliminf_set_eq :
+  bliminf s cofinite p = { x | { n | p n ∧ x ∉ s n }.finite } :=
+begin
+  rw ← compl_inj_iff,
+  simpa only [bliminf_eq_supr_binfi, compl_infi, compl_supr, ← blimsup_eq_infi_bsupr,
+    cofinite.blimsup_set_eq],
+end
+
+/-- In other words, `limsup cofinite s` is the set of elements lying inside the family `s`
+infinitely often. -/
+lemma cofinite.limsup_set_eq :
+  limsup s cofinite = { x | { n | x ∈ s n }.infinite } :=
+by simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]
+
+/-- In other words, `liminf cofinite s` is the set of elements lying outside the family `s`
+finitely often. -/
+lemma cofinite.liminf_set_eq :
+  liminf s cofinite = { x | { n | x ∉ s n }.finite } :=
+by simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]
+
+end set_lattice
+
 section conditionally_complete_linear_order
 
 lemma frequently_lt_of_lt_Limsup {f : filter α} [conditionally_complete_linear_order α] {a : α}
-  (hf : f.is_cobounded (≤) . is_bounded_default) (h : a < f.Limsup) : ∃ᶠ n in f, a < n :=
+  (hf : f.is_cobounded (≤) . is_bounded_default) (h : a < Limsup f) : ∃ᶠ n in f, a < n :=
 begin
   contrapose! h,
   simp only [not_frequently, not_lt] at h,
@@ -553,11 +729,11 @@ begin
 end
 
 lemma frequently_lt_of_Liminf_lt {f : filter α} [conditionally_complete_linear_order α] {a : α}
-  (hf : f.is_cobounded (≥) . is_bounded_default) (h : f.Liminf < a) : ∃ᶠ n in f, n < a :=
+  (hf : f.is_cobounded (≥) . is_bounded_default) (h : Liminf f < a) : ∃ᶠ n in f, n < a :=
 @frequently_lt_of_lt_Limsup (order_dual α) f _ a hf h
 
 lemma eventually_lt_of_lt_liminf {f : filter α} [conditionally_complete_linear_order β]
-  {u : α → β} {b : β} (h : b < liminf f u) (hu : f.is_bounded_under (≥) u . is_bounded_default) :
+  {u : α → β} {b : β} (h : b < liminf u f) (hu : f.is_bounded_under (≥) u . is_bounded_default) :
   ∀ᶠ a in f, b < u a :=
 begin
   obtain ⟨c, hc, hbc⟩ : ∃ (c : β) (hc : c ∈ {c : β | ∀ᶠ (n : α) in f, c ≤ u n}), b < c :=
@@ -566,14 +742,14 @@ begin
 end
 
 lemma eventually_lt_of_limsup_lt {f : filter α} [conditionally_complete_linear_order β]
-  {u : α → β} {b : β} (h : limsup f u < b) (hu : f.is_bounded_under (≤) u . is_bounded_default) :
+  {u : α → β} {b : β} (h : limsup u f < b) (hu : f.is_bounded_under (≤) u . is_bounded_default) :
   ∀ᶠ a in f, u a < b :=
 @eventually_lt_of_lt_liminf _ βᵒᵈ _ _ _ _ h hu
 
 lemma le_limsup_of_frequently_le {α β} [conditionally_complete_linear_order β] {f : filter α}
   {u : α → β}  {b : β} (hu_le : ∃ᶠ x in f, b ≤ u x)
   (hu : f.is_bounded_under (≤) u . is_bounded_default) :
-  b ≤ f.limsup u :=
+  b ≤ limsup u f :=
 begin
   revert hu_le,
   rw [←not_imp_not, not_frequently],
@@ -584,12 +760,12 @@ end
 lemma liminf_le_of_frequently_le  {α β} [conditionally_complete_linear_order β] {f : filter α}
   {u : α → β}  {b : β} (hu_le : ∃ᶠ x in f, u x ≤ b)
   (hu : f.is_bounded_under (≥) u . is_bounded_default) :
-  f.liminf u ≤ b :=
+  liminf u f ≤ b :=
 @le_limsup_of_frequently_le _ βᵒᵈ _ f u b hu_le hu
 
 lemma frequently_lt_of_lt_limsup {α β} [conditionally_complete_linear_order β] {f : filter α}
   {u : α → β}  {b : β}
-  (hu : f.is_cobounded_under (≤) u . is_bounded_default) (h : b < f.limsup u) :
+  (hu : f.is_cobounded_under (≤) u . is_bounded_default) (h : b < limsup u f) :
   ∃ᶠ x in f, b < u x :=
 begin
   contrapose! h,
@@ -599,7 +775,7 @@ end
 
 lemma frequently_lt_of_liminf_lt {α β} [conditionally_complete_linear_order β] {f : filter α}
   {u : α → β}  {b : β}
-  (hu : f.is_cobounded_under (≥) u . is_bounded_default) (h : f.liminf u < b) :
+  (hu : f.is_cobounded_under (≥) u . is_bounded_default) (h : liminf u f < b) :
   ∃ᶠ x in f, u x < b :=
 @frequently_lt_of_lt_limsup _ βᵒᵈ _ f u b hu h
 
@@ -644,7 +820,7 @@ lemma galois_connection.l_limsup_le [conditionally_complete_lattice β]
   {l : β → γ} {u : γ → β} (gc : galois_connection l u)
   (hlv : f.is_bounded_under (≤) (λ x, l (v x)) . is_bounded_default)
   (hv_co : f.is_cobounded_under (≤) v . is_bounded_default) :
-  l (f.limsup v) ≤ f.limsup (λ x, l (v x)) :=
+  l (limsup v f) ≤ limsup (λ x, l (v x)) f :=
 begin
   refine le_Limsup_of_le hlv (λ c hc, _),
   rw filter.eventually_map at hc,
@@ -658,10 +834,10 @@ lemma order_iso.limsup_apply {γ} [conditionally_complete_lattice β]
   (hu_co : f.is_cobounded_under (≤) u . is_bounded_default)
   (hgu : f.is_bounded_under (≤) (λ x, g (u x)) . is_bounded_default)
   (hgu_co : f.is_cobounded_under (≤) (λ x, g (u x)) . is_bounded_default) :
-  g (f.limsup u) = f.limsup (λ x, g (u x)) :=
+  g (limsup u f) = limsup (λ x, g (u x)) f :=
 begin
   refine le_antisymm (g.to_galois_connection.l_limsup_le hgu hu_co) _,
-  rw [←(g.symm.symm_apply_apply (f.limsup (λ (x : α), g (u x)))), g.symm_symm],
+  rw [←(g.symm.symm_apply_apply $ limsup (λ x, g (u x)) f), g.symm_symm],
   refine g.monotone _,
   have hf : u = λ i, g.symm (g (u i)), from funext (λ i, (g.symm_apply_apply (u i)).symm),
   nth_rewrite 0 hf,
@@ -676,7 +852,7 @@ lemma order_iso.liminf_apply {γ} [conditionally_complete_lattice β]
   (hu_co : f.is_cobounded_under (≥) u . is_bounded_default)
   (hgu : f.is_bounded_under (≥) (λ x, g (u x)) . is_bounded_default)
   (hgu_co : f.is_cobounded_under (≥) (λ x, g (u x)) . is_bounded_default) :
-  g (f.liminf u) = f.liminf (λ x, g (u x)) :=
+  g (liminf u f) = liminf (λ x, g (u x)) f :=
 @order_iso.limsup_apply α βᵒᵈ γᵒᵈ _ _ f u g.dual hu hu_co hgu hgu_co
 
 end order
diff --git a/src/probability/martingale/borel_cantelli.lean b/src/probability/martingale/borel_cantelli.lean
index ba26caf71b6ad..d2c1a9641fdbc 100644
--- a/src/probability/martingale/borel_cantelli.lean
+++ b/src/probability/martingale/borel_cantelli.lean
@@ -389,7 +389,7 @@ filtration `ℱ` such that for all `n`, `s n` is `ℱ n`-measurable, `at_top.lim
 everywhere equal to the set for which `∑ k, ℙ(s (k + 1) | ℱ k) = ∞`. -/
 theorem ae_mem_limsup_at_top_iff [is_finite_measure μ]
   {s : ℕ → set Ω} (hs : ∀ n, measurable_set[ℱ n] (s n)) :
-  ∀ᵐ ω ∂μ, ω ∈ limsup at_top s ↔
+  ∀ᵐ ω ∂μ, ω ∈ limsup s at_top ↔
     tendsto (λ n, ∑ k in finset.range n, μ[(s (k + 1)).indicator (1 : Ω → ℝ) | ℱ k] ω)
       at_top at_top :=
 (limsup_eq_tendsto_sum_indicator_at_top ℝ s).symm ▸ tendsto_sum_indicator_at_top_iff' hs
diff --git a/src/probability/martingale/convergence.lean b/src/probability/martingale/convergence.lean
index d29bc0750b90a..012be9ecce518 100644
--- a/src/probability/martingale/convergence.lean
+++ b/src/probability/martingale/convergence.lean
@@ -136,7 +136,7 @@ convergent.
 We use the spelling `< ∞` instead of the standard `≠ ∞` in the assumptions since it is not as easy
 to change `<` to `≠` under binders. -/
 lemma tendsto_of_uncrossing_lt_top
-  (hf₁ : liminf at_top (λ n, (∥f n ω∥₊ : ℝ≥0∞)) < ∞)
+  (hf₁ : liminf (λ n, (∥f n ω∥₊ : ℝ≥0∞)) at_top < ∞)
   (hf₂ : ∀ a b : ℚ, a < b → upcrossings a b f ω < ∞) :
   ∃ c, tendsto (λ n, f n ω) at_top (𝓝 c) :=
 begin
diff --git a/src/topology/algebra/order/liminf_limsup.lean b/src/topology/algebra/order/liminf_limsup.lean
index a50d7c1808ed9..5200a03484d2f 100644
--- a/src/topology/algebra/order/liminf_limsup.lean
+++ b/src/topology/algebra/order/liminf_limsup.lean
@@ -151,18 +151,18 @@ theorem Limsup_eq_of_le_nhds : ∀ {f : filter α} {a : α} [ne_bot f], f ≤ 
 
 /-- If a function has a limit, then its limsup coincides with its limit. -/
 theorem filter.tendsto.limsup_eq {f : filter β} {u : β → α} {a : α} [ne_bot f]
-  (h : tendsto u f (𝓝 a)) : limsup f u = a :=
+  (h : tendsto u f (𝓝 a)) : limsup u f = a :=
 Limsup_eq_of_le_nhds h
 
 /-- If a function has a limit, then its liminf coincides with its limit. -/
 theorem filter.tendsto.liminf_eq {f : filter β} {u : β → α} {a : α} [ne_bot f]
-  (h : tendsto u f (𝓝 a)) : liminf f u = a :=
+  (h : tendsto u f (𝓝 a)) : liminf u f = a :=
 Liminf_eq_of_le_nhds h
 
 /-- 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 : α}
-  (hinf : liminf f u = a) (hsup : limsup f u = a)
+  (hinf : liminf u f = a) (hsup : limsup u f = a)
   (h : f.is_bounded_under (≤) u . is_bounded_default)
   (h' : f.is_bounded_under (≥) u . is_bounded_default) :
   tendsto u f (𝓝 a) :=
@@ -171,7 +171,7 @@ le_nhds_of_Limsup_eq_Liminf h h' 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)
+  (hinf : a ≤ liminf u f) (hsup : limsup u f ≤ a)
   (h : f.is_bounded_under (≤) u . is_bounded_default)
   (h' : f.is_bounded_under (≥) u . is_bounded_default) :
   tendsto u f (𝓝 a) :=
@@ -193,7 +193,7 @@ lemma tendsto_of_no_upcrossings [densely_ordered α]
 begin
   by_cases hbot : f = ⊥, { rw hbot, exact ⟨Inf ∅, tendsto_bot⟩ },
   haveI : ne_bot f := ⟨hbot⟩,
-  refine ⟨limsup f u, _⟩,
+  refine ⟨limsup u f, _⟩,
   apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h',
   by_contra' hlt,
   obtain ⟨a, ⟨⟨la, au⟩, as⟩⟩ : ∃ a, (f.liminf u < a ∧ a < f.limsup u) ∧ a ∈ s :=
@@ -324,7 +324,7 @@ section indicator
 open_locale big_operators
 
 lemma limsup_eq_tendsto_sum_indicator_nat_at_top (s : ℕ → set α) :
-  limsup at_top s =
+  limsup s at_top =
     {ω | tendsto (λ n, ∑ k in finset.range n, (s (k + 1)).indicator (1 : α → ℕ) ω) at_top at_top} :=
 begin
   ext ω,
@@ -383,7 +383,7 @@ end
 
 lemma limsup_eq_tendsto_sum_indicator_at_top
   (R : Type*) [strict_ordered_semiring R] [nontrivial R] [archimedean R] (s : ℕ → set α) :
-  limsup at_top s =
+  limsup s at_top =
     {ω | tendsto (λ n, ∑ k in finset.range n, (s (k + 1)).indicator (1 : α → R) ω) at_top at_top} :=
 begin
   rw limsup_eq_tendsto_sum_indicator_nat_at_top s,
diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean
index 89a7b6f46ff5f..eda048d0cf97a 100644
--- a/src/topology/instances/ennreal.lean
+++ b/src/topology/instances/ennreal.lean
@@ -488,11 +488,11 @@ lemma inv_map_supr {ι : Sort*} {x : ι → ℝ≥0∞} :
 order_iso.inv_ennreal.map_supr x
 
 lemma inv_limsup {ι : Sort*} {x : ι → ℝ≥0∞} {l : filter ι} :
-  (l.limsup x)⁻¹ = l.liminf (λ i, (x i)⁻¹) :=
+  (limsup x l)⁻¹ = liminf (λ i, (x i)⁻¹) l :=
 by simp only [limsup_eq_infi_supr, inv_map_infi, inv_map_supr, liminf_eq_supr_infi]
 
 lemma inv_liminf {ι : Sort*} {x : ι → ℝ≥0∞} {l : filter ι} :
-  (l.liminf x)⁻¹ = l.limsup (λ i, (x i)⁻¹) :=
+  (liminf x l)⁻¹ = limsup (λ i, (x i)⁻¹) l :=
 by simp only [limsup_eq_infi_supr, inv_map_infi, inv_map_supr, liminf_eq_supr_infi]
 
 instance : has_continuous_inv ℝ≥0∞ := ⟨order_iso.inv_ennreal.continuous⟩
@@ -654,7 +654,7 @@ end topological_space
 section liminf
 
 lemma exists_frequently_lt_of_liminf_ne_top
-  {ι : Type*} {l : filter ι} {x : ι → ℝ} (hx : liminf l (λ n, (∥x n∥₊ : ℝ≥0∞)) ≠ ∞) :
+  {ι : Type*} {l : filter ι} {x : ι → ℝ} (hx : liminf (λ n, (∥x n∥₊ : ℝ≥0∞)) l ≠ ∞) :
   ∃ R, ∃ᶠ n in l, x n < R :=
 begin
   by_contra h,
@@ -665,7 +665,7 @@ begin
 end
 
 lemma exists_frequently_lt_of_liminf_ne_top'
-  {ι : Type*} {l : filter ι} {x : ι → ℝ} (hx : liminf l (λ n, (∥x n∥₊ : ℝ≥0∞)) ≠ ∞) :
+  {ι : Type*} {l : filter ι} {x : ι → ℝ} (hx : liminf (λ n, (∥x n∥₊ : ℝ≥0∞)) l ≠ ∞) :
   ∃ R, ∃ᶠ n in l, R < x n :=
 begin
   by_contra h,
@@ -677,7 +677,7 @@ end
 
 lemma exists_upcrossings_of_not_bounded_under
   {ι : Type*} {l : filter ι} {x : ι → ℝ}
-  (hf : liminf l (λ i, (∥x i∥₊ : ℝ≥0∞)) ≠ ∞)
+  (hf : liminf (λ i, (∥x i∥₊ : ℝ≥0∞)) l ≠ ∞)
   (hbdd : ¬ is_bounded_under (≤) l (λ i, |x i|)) :
   ∃ a b : ℚ, a < b ∧ (∃ᶠ i in l, x i < a) ∧ (∃ᶠ i in l, ↑b < x i) :=
 begin
@@ -783,7 +783,7 @@ protected lemma tsum_eq_supr_nat {f : ℕ → ℝ≥0∞} :
 ennreal.tsum_eq_supr_sum' _ finset.exists_nat_subset_range
 
 protected lemma tsum_eq_liminf_sum_nat {f : ℕ → ℝ≥0∞} :
-  ∑' i, f i = filter.at_top.liminf (λ n, ∑ i in finset.range n, f i) :=
+  ∑' i, f i = liminf (λ n, ∑ i in finset.range n, f i) at_top :=
 begin
   rw [ennreal.tsum_eq_supr_nat, filter.liminf_eq_supr_infi_of_nat],
   congr,
diff --git a/src/topology/metric_space/hausdorff_dimension.lean b/src/topology/metric_space/hausdorff_dimension.lean
index fcfcd22bc4213..976e0f419be16 100644
--- a/src/topology/metric_space/hausdorff_dimension.lean
+++ b/src/topology/metric_space/hausdorff_dimension.lean
@@ -226,7 +226,7 @@ end
 /-- In an (extended) metric space with second countable topology, the Hausdorff dimension
 of a set `s` is the supremum over `x ∈ s` of the limit superiors of `dimH t` along
 `(𝓝[s] x).small_sets`. -/
-lemma bsupr_limsup_dimH (s : set X) : (⨆ x ∈ s, limsup (𝓝[s] x).small_sets dimH) = dimH s :=
+lemma bsupr_limsup_dimH (s : set X) : (⨆ x ∈ s, limsup dimH (𝓝[s] x).small_sets) = dimH s :=
 begin
   refine le_antisymm (supr₂_le $ λ x hx, _) _,
   { refine Limsup_le_of_le (by apply_auto_param) (eventually_map.2 _),
@@ -241,7 +241,7 @@ end
 /-- In an (extended) metric space with second countable topology, the Hausdorff dimension
 of a set `s` is the supremum over all `x` of the limit superiors of `dimH t` along
 `(𝓝[s] x).small_sets`. -/
-lemma supr_limsup_dimH (s : set X) : (⨆ x, limsup (𝓝[s] x).small_sets dimH) = dimH s :=
+lemma supr_limsup_dimH (s : set X) : (⨆ x, limsup dimH (𝓝[s] x).small_sets) = dimH s :=
 begin
   refine le_antisymm (supr_le $ λ x, _) _,
   { refine Limsup_le_of_le (by apply_auto_param) (eventually_map.2 _),