feat: liminf and limsup add/mul lemmas in Real

Mathlib/Algebra/Order/Field/Basic.lean

@@ -747,6 +747,47 @@ theorem le_of_forall_sub_le (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a := by
   simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using
     exists_add_lt_and_pos_of_lt h
 
+private lemma exists_lt_mul_left_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
+    ∃ a' ∈ Set.Ico 0 a, c < a' * b := by
+  rcases eq_or_lt_of_le ha with rfl | ha
+  · rw [zero_mul] at h; exact (not_le_of_lt h hc).rec
+  rcases lt_trichotomy b 0 with hb | rfl | hb
+  · exact (not_le_of_lt (h.trans (mul_neg_of_pos_of_neg ha hb)) hc).rec
+  · rw [mul_zero] at h; exact (not_le_of_lt h hc).rec
+  · obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)
+    exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩
+
+private lemma exists_lt_mul_right_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
+    ∃ b' ∈ Set.Ico 0 b, c < a * b' := by
+  have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
+  simp_rw [mul_comm a] at h ⊢
+  exact exists_lt_mul_left_of_nonneg hb.le hc h
+
+private lemma exists_mul_left_lt₀ {a b c : α} (hc : a * b < c) : ∃ a' > a, a' * b < c := by
+  rcases le_or_lt b 0 with hb | hb
+  · obtain ⟨a', ha'⟩ := exists_gt a
+    exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩
+  · obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)
+    exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩
+
+private lemma exists_mul_right_lt₀ {a b c : α} (hc : a * b < c) : ∃ b' > b, a * b' < c := by
+  simp_rw [mul_comm a] at hc ⊢; exact exists_mul_left_lt₀ hc
+
+lemma le_mul_of_forall_lt₀ {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b := by
+  refine le_of_forall_le_of_dense fun d hd ↦ ?_
+  obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd
+  obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd
+  exact (h a' ha' b' hb').trans hd.le
+
+lemma mul_le_of_forall_lt_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c)
+    (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c := by
+  refine le_of_forall_ge_of_dense fun d d_ab ↦ ?_
+  rcases lt_or_le d 0 with hd | hd
+  · exact hd.le.trans hc
+  obtain ⟨a', ha', d_ab⟩ := exists_lt_mul_left_of_nonneg ha hd d_ab
+  obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab
+  exact d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)
+
 theorem mul_self_inj_of_nonneg (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b :=
   mul_self_eq_mul_self_iff.trans <|
     or_iff_left_of_imp fun h => by

Mathlib/Algebra/Order/Group/DenselyOrdered.lean

@@ -11,7 +11,6 @@ import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 # Lemmas about densely linearly ordered groups.
 -/
 
-
 variable {α : Type*}
 
 section DenselyOrdered
@@ -38,3 +37,53 @@ theorem le_iff_forall_lt_one_mul_le : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b :=
   le_iff_forall_one_lt_le_mul (α := αᵒᵈ)
 
 end DenselyOrdered
+
+section DenselyOrdered
+
+@[to_additive]
+private lemma exists_lt_mul_left [Group α] [LT α] [DenselyOrdered α]
+    [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a b c : α} (hc : c < a * b) :
+    ∃ a' < a, c < a' * b := by
+  obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul.2 hc)
+  exact ⟨a', ha', div_lt_iff_lt_mul.1 hc'⟩
+
+@[to_additive]
+private lemma exists_lt_mul_right [CommGroup α] [LT α] [DenselyOrdered α]
+    [CovariantClass α α (· * ·) (· < ·)] {a b c : α} (hc : c < a * b) :
+    ∃ b' < b, c < a * b' := by
+  obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul'.2 hc)
+  exact ⟨a', ha', div_lt_iff_lt_mul'.1 hc'⟩
+
+@[to_additive]
+private lemma exists_mul_left_lt [Group α] [LT α] [DenselyOrdered α]
+    [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a b c : α} (hc : a * b < c) :
+    ∃ a' > a, a' * b < c := by
+  obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt.2 hc)
+  exact ⟨a', ha', lt_div_iff_mul_lt.1 hc'⟩
+
+@[to_additive]
+private lemma exists_mul_right_lt [CommGroup α] [LT α] [DenselyOrdered α]
+    [CovariantClass α α (· * ·) (· < ·)] {a b c : α} (hc : a * b < c) :
+    ∃ b' > b, a * b' < c := by
+  obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt'.2 hc)
+  exact ⟨a', ha', lt_div_iff_mul_lt'.1 hc'⟩
+
+@[to_additive]
+lemma le_mul_of_forall_lt [CommGroup α] [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+    [DenselyOrdered α] {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') :
+    c ≤ a * b := by
+  refine le_of_forall_le_of_dense fun d hd ↦ ?_
+  obtain ⟨a', ha', hd⟩ := exists_mul_left_lt hd
+  obtain ⟨b', hb', hd⟩ := exists_mul_right_lt hd
+  exact (h a' ha' b' hb').trans hd.le
+
+@[to_additive]
+lemma mul_le_of_forall_lt [CommGroup α] [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+    [DenselyOrdered α] {a b c : α} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) :
+    a * b ≤ c := by
+  refine le_of_forall_ge_of_dense fun d hd ↦ ?_
+  obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
+  obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
+  exact hd.le.trans (h a' ha' b' hb')
+
+end DenselyOrdered

Mathlib/Order/LiminfLimsup.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel, Johannes Hölzl, Rémy Degenne
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.Unbundled.Abs
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import Mathlib.Order.Filter.Cofinite
 import Mathlib.Order.Hom.CompleteLattice
 
@@ -111,6 +112,22 @@ theorem IsBoundedUnder.comp {l : Filter γ} {q : β → β → Prop} {u : γ →
 section Preorder
 variable [Preorder α] {f : Filter β} {u : β → α} {s : Set β}
 
+lemma IsBoundedUnder.eventually_le (h : IsBoundedUnder (· ≤ ·) f u) :
+    ∃ a, ∀ᶠ x in f, u x ≤ a := by
+  obtain ⟨a, ha⟩ := h
+  use a
+  exact eventually_map.1 ha
+
+lemma IsBoundedUnder.eventually_ge (h : IsBoundedUnder (· ≥ ·) f u) :
+    ∃ a, ∀ᶠ x in f, a ≤ u x :=
+  IsBoundedUnder.eventually_le (α := αᵒᵈ) h
+
+lemma isBoundedUnder_of_eventually_le {a : α} (h : ∀ᶠ x in f, u x ≤ a) :
+    IsBoundedUnder (· ≤ ·) f u := ⟨a, h⟩
+
+lemma isBoundedUnder_of_eventually_ge {a : α} (h : ∀ᶠ x in f, a ≤ u x) :
+    IsBoundedUnder (· ≥ ·) f u := ⟨a, h⟩
+
 lemma isBoundedUnder_iff_eventually_bddAbove :
     f.IsBoundedUnder (· ≤ ·) u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ x in f, x ∈ s := by
   constructor
@@ -281,6 +298,57 @@ theorem isCobounded_principal (s : Set α) :
 theorem IsCobounded.mono (h : f ≤ g) : f.IsCobounded r → g.IsCobounded r
   | ⟨b, hb⟩ => ⟨b, fun a ha => hb a (h ha)⟩
 
+/-- For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness
+from below. -/
+lemma IsCobounded.frequently_ge [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≤ ·) f) :
+    ∃ l, ∃ᶠ x in f, l ≤ x := by
+  obtain ⟨t, ht⟩ := cobdd
+  rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
+  · exact ⟨t, .of_forall fun r ↦ tbot r⟩
+  refine ⟨t', fun ev ↦ ?_⟩
+  specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
+  exact not_lt_of_le ht ht'
+
+/-- For nontrivial filters in linear orders, coboundedness for `≥` implies frequent boundedness
+from above. -/
+lemma IsCobounded.frequently_le [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≥ ·) f) :
+    ∃ u, ∃ᶠ x in f, x ≤ u :=
+  cobdd.frequently_ge (α := αᵒᵈ)
+
+/-- In linear orders, frequent boundedness from below implies coboundedness for `≤`. -/
+lemma IsCobounded.of_frequently_ge [LinearOrder α] {l : α} (freq_ge : ∃ᶠ x in f, l ≤ x) :
+    IsCobounded (· ≤ ·) f := by
+  rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩
+  · exact ⟨l, fun x _ ↦ lbot x⟩
+  refine ⟨l', fun u hu ↦ ?_⟩
+  obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists
+  exact hl'.le.trans (l_le_w.trans w_le_u)
+
+/-- In linear orders, frequent boundedness from above implies coboundedness for `≥`. -/
+lemma IsCobounded.of_frequently_le [LinearOrder α] {u : α} (freq_le : ∃ᶠ r in f, r ≤ u) :
+    IsCobounded (· ≥ ·) f :=
+  IsCobounded.of_frequently_ge (α := αᵒᵈ) freq_le
+
+lemma IsCoboundedUnder.frequently_ge [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α}
+    (h : IsCoboundedUnder (· ≤ ·) f u) :
+    ∃ a, ∃ᶠ x in f, a ≤ u x :=
+  IsCobounded.frequently_ge h
+
+lemma IsCoboundedUnder.frequently_le [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α}
+    (h : IsCoboundedUnder (· ≥ ·) f u) :
+    ∃ a, ∃ᶠ x in f, u x ≤ a :=
+  IsCobounded.frequently_le h
+
+lemma IsCoboundedUnder.of_frequently_ge [LinearOrder α] {f : Filter ι} {u : ι → α}
+    {a : α} (freq_ge : ∃ᶠ x in f, a ≤ u x) :
+    IsCoboundedUnder (· ≤ ·) f u :=
+  IsCobounded.of_frequently_ge freq_ge
+
+lemma IsCoboundedUnder.of_frequently_le [LinearOrder α] {f : Filter ι} {u : ι → α}
+    {a : α} (freq_le : ∃ᶠ x in f, u x ≤ a) :
+    IsCoboundedUnder (· ≥ ·) f u :=
+  IsCobounded.of_frequently_le freq_le
+
 end Relation
 
 section add_and_sum
@@ -328,20 +396,70 @@ lemma isBoundedUnder_le_add [Add R]
 lemma isBoundedUnder_le_sum {κ : Type*} [AddCommMonoid R]
     [CovariantClass R R (fun a b ↦ a + b) (· ≤ ·)] [CovariantClass R R (fun a b ↦ b + a) (· ≤ ·)]
     {u : κ → α → R} (s : Finset κ) :
-    (∀ k ∈ s, f.IsBoundedUnder (· ≤ ·) (u k)) → f.IsBoundedUnder (· ≤ ·) (∑ k ∈ s, u k) := by
-  apply isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_le_add) le_rfl
+    (∀ k ∈ s, f.IsBoundedUnder (· ≤ ·) (u k)) → f.IsBoundedUnder (· ≤ ·) (∑ k ∈ s, u k) :=
+  fun h ↦ isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_le_add) le_rfl s h
 
 lemma isBoundedUnder_ge_sum {κ : Type*} [AddCommMonoid R]
     [CovariantClass R R (fun a b ↦ a + b) (· ≤ ·)] [CovariantClass R R (fun a b ↦ b + a) (· ≤ ·)]
     {u : κ → α → R} (s : Finset κ) :
     (∀ k ∈ s, f.IsBoundedUnder (· ≥ ·) (u k)) →
-      f.IsBoundedUnder (· ≥ ·) (∑ k ∈ s, u k) := by
-  haveI aux : CovariantClass R R (fun a b ↦ a + b) (· ≥ ·) :=
-    { elim := fun x _ _ hy ↦ add_le_add_left hy x }
-  apply isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_ge_add) le_rfl
+      f.IsBoundedUnder (· ≥ ·) (∑ k ∈ s, u k) :=
+  fun h ↦ isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_ge_add) le_rfl s h
+
+end add_and_sum
+
+section add_and_sum
+
+variable {α : Type*} {R : Type*} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot]
+  [CovariantClass R R (fun a b ↦ a + b) (· ≤ ·)] [CovariantClass R R (fun a b ↦ b + a) (· ≤ ·)]
+  {u v : α → R}
+
+lemma isCoboundedUnder_ge_add (hu : f.IsBoundedUnder (· ≤ ·) u)
+    (hv : f.IsCoboundedUnder (· ≥ ·) v) :
+    f.IsCoboundedUnder (· ≥ ·) (u + v) := by
+  obtain ⟨U, hU⟩ := hu.eventually_le
+  obtain ⟨V, hV⟩ := hv.frequently_le
+  apply IsCoboundedUnder.of_frequently_le (a := U + V)
+  exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1
+
+lemma isCoboundedUnder_le_add (hu : f.IsBoundedUnder (· ≥ ·) u)
+    (hv : f.IsCoboundedUnder (· ≤ ·) v) :
+    f.IsCoboundedUnder (· ≤ ·) (u + v) := by
+  obtain ⟨U, hU⟩ := hu.eventually_ge
+  obtain ⟨V, hV⟩ := hv.frequently_ge
+  apply IsCoboundedUnder.of_frequently_ge (a := U + V)
+  exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1
 
 end add_and_sum
 
+section mul
+
+lemma isBoundedUnder_le_mul_of_nonneg [Mul α] [Zero α] [Preorder α] [PosMulMono α]
+    [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u)
+    (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
+    (h₃ : 0 ≤ᶠ[f] v)
+    (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) :
+    IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v) := by
+  obtain ⟨U, hU⟩ := h₂.eventually_le
+  obtain ⟨V, hV⟩ := h₄.eventually_le
+  refine isBoundedUnder_of_eventually_le (a := U * V) ?_
+  filter_upwards [hU, hV, h₁, h₃] with x x_U x_V u_0 v_0
+  exact mul_le_mul x_U x_V v_0 (u_0.trans x_U)
+
+lemma isCoboundedUnder_ge_mul_of_nonneg [Mul α] [Zero α] [LinearOrder α] [PosMulMono α]
+    [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u)
+    (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
+    (h₃ : 0 ≤ᶠ[f] v)
+    (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
+    IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f (u * v) := by
+  obtain ⟨U, hU⟩ := h₂.eventually_le
+  obtain ⟨V, hV⟩ := h₄.frequently_le
+  exact IsCoboundedUnder.of_frequently_le (a := U * V)
+    <| (hV.and_eventually (hU.and (h₁.and h₃))).mono fun x ⟨x_V, x_U, u_0, v_0⟩ ↦
+    mul_le_mul x_U x_V v_0 (u_0.trans x_U)
+
+end mul
+
 section Nonempty
 variable [Preorder α] [Nonempty α] {f : Filter β} {u : β → α}
 
@@ -1642,50 +1760,6 @@ section frequently_bounded
 
 variable {R S : Type*} {F : Filter R} [LinearOrder R] [LinearOrder S]
 
-namespace Filter
-
-/-- For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness
-from below. -/
-lemma IsCobounded.frequently_ge [NeBot F] (cobdd : IsCobounded (· ≤ ·) F) :
-    ∃ l, ∃ᶠ x in F, l ≤ x := by
-  obtain ⟨t, ht⟩ := cobdd
-  by_cases tbot : IsBot t
-  · refine ⟨t, Frequently.of_forall fun r ↦ tbot r⟩
-  obtain ⟨t', ht'⟩ : ∃ t', t' < t := by
-    by_contra!
-    exact tbot this
-  refine ⟨t', ?_⟩
-  intro ev
-  specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
-  apply lt_irrefl t' <| lt_of_lt_of_le ht' ht
-
-/-- For nontrivial filters in linear orders, coboundedness for `≥` implies frequent boundedness
-from above. -/
-lemma IsCobounded.frequently_le [NeBot F] (cobdd : IsCobounded (· ≥ ·) F) :
-    ∃ u, ∃ᶠ x in F, x ≤ u :=
-  cobdd.frequently_ge (R := Rᵒᵈ)
-
-/-- In linear orders, frequent boundedness from below implies coboundedness for `≤`. -/
-lemma IsCobounded.of_frequently_ge {l : R} (freq_ge : ∃ᶠ x in F, l ≤ x) :
-    IsCobounded (· ≤ ·) F := by
-  by_cases lbot : IsBot l
-  · refine ⟨l, fun x _ ↦ lbot x⟩
-  obtain ⟨l', hl'⟩ : ∃ l', l' < l := by
-    by_contra!
-    exact lbot this
-  refine ⟨l', ?_⟩
-  intro u hu
-  have key : ∃ᶠ x in F, l ≤ x ∧ x ≤ u := Frequently.and_eventually freq_ge hu
-  obtain ⟨w, l_le_w, w_le_u⟩ := key.exists
-  exact hl'.le.trans <| l_le_w.trans w_le_u
-
-/-- In linear orders, frequent boundedness from above implies coboundedness for `≥`. -/
-lemma IsCobounded.of_frequently_le {u : R} (freq_le : ∃ᶠ r in F, r ≤ u) :
-    IsCobounded (· ≥ ·) F :=
-  IsCobounded.of_frequently_ge (R := Rᵒᵈ) freq_le
-
-end Filter
-
 lemma Monotone.frequently_ge_map_of_frequently_ge {f : R → S} (f_incr : Monotone f)
     {l : R} (freq_ge : ∃ᶠ x in F, l ≤ x) :
     ∃ᶠ x' in F.map f, f l ≤ x' := by
@@ -1737,4 +1811,4 @@ lemma Antitone.isCoboundedUnder_ge_of_isCobounded {f : R → S} (f_decr : Antito
 
 end frequently_bounded
 
-set_option linter.style.longFile 1800
+set_option linter.style.longFile 1900