feat(order/liminf_limsup): liminf_nat_add and liminf_le_of_frequently…

…_le' (#6220)

Add `liminf_nat_add (f : ℕ → α) (k : ℕ) : at_top.liminf f = at_top.liminf (λ i, f (i + k))`. Same for `limsup`.

Add `liminf_le_of_frequently_le'`, variant of `liminf_le_of_frequently_le` in which the lattice is complete but there is no linear order. Same for `limsup`.

src/order/complete_lattice.lean

@@ -913,6 +913,20 @@ end
 lemma infi_ge_eq_infi_nat_add {u : ℕ → α} (n : ℕ) : (⨅ i ≥ n, u i) = ⨅ i, u (i + n) :=
 @supr_ge_eq_supr_nat_add (order_dual α) _ _ _
 
+lemma monotone.supr_nat_add {f : ℕ → α} (hf : monotone f) (k : ℕ) :
+  (⨆ n, f (n + k)) = ⨆ n, f n :=
+le_antisymm (supr_le (λ i, (le_refl _).trans (le_supr _ (i + k))))
+    (supr_le_supr (λ i, hf (nat.le_add_right i k)))
+
+@[simp] lemma supr_infi_ge_nat_add (f : ℕ → α) (k : ℕ) :
+  (⨆ n, ⨅ i ≥ n, f (i + k)) = ⨆ n, ⨅ i ≥ n, f i :=
+begin
+  have hf : monotone (λ n, ⨅ i ≥ n, f i),
+    from λ n m hnm, le_infi (λ i, (infi_le _ i).trans (le_infi (λ h, infi_le _ (hnm.trans h)))),
+  rw ←monotone.supr_nat_add hf k,
+  { simp_rw [infi_ge_eq_infi_nat_add, ←nat.add_assoc], },
+end
+
 end
 
 section complete_linear_order

src/order/liminf_limsup.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel, Johannes Hölzl
+Authors: Sébastien Gouëzel, Johannes Hölzl, Rémy Degenne
 -/
 import order.filter.partial
 import order.filter.at_top_bot
@@ -365,6 +365,32 @@ theorem has_basis.liminf_eq_supr_infi {p : ι → Prop} {s : ι → set β} {f :
   (h : f.has_basis p s) : f.liminf u = ⨆ i (hi : p i), ⨅ a ∈ s i, u a :=
 @has_basis.limsup_eq_infi_supr (order_dual α) _ _ _ _ _ _ _ h
 
+@[simp] lemma liminf_nat_add (f : ℕ → α) (k : ℕ) :
+  at_top.liminf (λ i, f (i + k)) = at_top.liminf f :=
+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 :=
+@liminf_nat_add (order_dual α) _ 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 :=
+begin
+  rw liminf_eq,
+  refine Sup_le (λ b hb, _),
+  have hbx : ∃ᶠ a in f, b ≤ x,
+  { revert h,
+    rw [←not_imp_not, not_frequently, not_frequently],
+    exact λ h, hb.mp (h.mono (λ a hbx hba hax, hbx (hba.trans hax))), },
+  exact hbx.exists.some_spec,
+end
+
+lemma le_limsup_of_frequently_le' {α β} [complete_lattice β]
+  {f : filter α} {u : α → β} {x : β} (h : ∃ᶠ a in f, x ≤ u a) :
+  x ≤ f.limsup u :=
+@liminf_le_of_frequently_le' _ (order_dual β) _ _ _ _ h
+
 end complete_lattice
 
 section conditionally_complete_linear_order