feat: Eventual boundedness of neighborhoods (#8009)

Forward port leanprover-community/mathlib#18629




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Order/Filter/Pi.lean

@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov, Alex Kontorovich
 -/
 import Mathlib.Order.Filter.Bases
 
-#align_import order.filter.pi from "leanprover-community/mathlib"@"1f0096e6caa61e9c849ec2adbd227e960e9dff58"
+#align_import order.filter.pi from "leanprover-community/mathlib"@"ce64cd319bb6b3e82f31c2d38e79080d377be451"
 
 /-!
 # (Co)product of a family of filters
@@ -29,6 +29,7 @@ open Classical Filter
 namespace Filter
 
 variable {ι : Type*} {α : ι → Type*} {f f₁ f₂ : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)}
+  {p : ∀ i, α i → Prop}
 
 section Pi
 
@@ -103,6 +104,14 @@ theorem pi_mem_pi_iff [∀ i, NeBot (f i)] {I : Set ι} (hI : I.Finite) :
   ⟨fun h _i hi => mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩
 #align filter.pi_mem_pi_iff Filter.pi_mem_pi_iff
 
+theorem Eventually.eval_pi {i : ι} (hf : ∀ᶠ x : α i in f i, p i x) :
+    ∀ᶠ x : ∀ i : ι, α i in pi f, p i (x i) := (tendsto_eval_pi _ _).eventually hf
+#align filter.eventually.eval_pi Filter.Eventually.eval_pi
+
+theorem eventually_pi [Finite ι] (hf : ∀ i, ∀ᶠ x in f i, p i x) :
+    ∀ᶠ x : ∀ i, α i in pi f, ∀ i, p i (x i) := eventually_all.2 fun _i => (hf _).eval_pi
+#align filter.eventually_pi Filter.eventually_pi
+
 theorem hasBasis_pi {ι' : ι → Type} {s : ∀ i, ι' i → Set (α i)} {p : ∀ i, ι' i → Prop}
     (h : ∀ i, (f i).HasBasis (p i) (s i)) :
     (pi f).HasBasis (fun If : Set ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i))

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
+Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov, Yaël Dillies
 -/
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Order
@@ -12,91 +12,168 @@ import Mathlib.Order.Filter.Archimedean
 import Mathlib.Order.Filter.CountableInter
 import Mathlib.Topology.Order.Basic
 
-#align_import topology.algebra.order.liminf_limsup from "leanprover-community/mathlib"@"ffde2d8a6e689149e44fd95fa862c23a57f8c780"
+#align_import topology.algebra.order.liminf_limsup from "leanprover-community/mathlib"@"ce64cd319bb6b3e82f31c2d38e79080d377be451"
 
 /-!
 # Lemmas about liminf and limsup in an order topology.
+
+## Main declarations
+
+* `BoundedLENhdsClass`: Typeclass stating that neighborhoods are eventually bounded above.
+* `BoundedGENhdsClass`: Typeclass stating that neighborhoods are eventually bounded below.
+
+## Implementation notes
+
+The same lemmas are true in `ℝ`, `ℝ × ℝ`, `ι → ℝ`, `EuclideanSpace ι ℝ`. To avoid code
+duplication, we provide an ad hoc axiomatisation of the properties we need.
 -/
 
 
 open Filter TopologicalSpace
 
-open Topology Classical
+open scoped Topology Classical
 
 universe u v
 
-variable {α : Type u} {β : Type v}
+variable {ι α β R S : Type*} {π : ι → Type*}
 
-section LiminfLimsup
+/-- Ad hoc typeclass stating that neighborhoods are eventually bounded above. -/
+class BoundedLENhdsClass (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
+  isBounded_le_nhds (a : α) : (𝓝 a).IsBounded (· ≤ ·)
+#align bounded_le_nhds_class BoundedLENhdsClass
+
+/-- Ad hoc typeclass stating that neighborhoods are eventually bounded below. -/
+class BoundedGENhdsClass (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
+  isBounded_ge_nhds (a : α) : (𝓝 a).IsBounded (· ≥ ·)
+#align bounded_ge_nhds_class BoundedGENhdsClass
 
-section OrderClosedTopology
+section Preorder
+variable [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
 
-variable [SemilatticeSup α] [TopologicalSpace α] [OrderTopology α]
+section BoundedLENhdsClass
+variable [BoundedLENhdsClass α] [BoundedLENhdsClass β] {f : Filter ι} {u : ι → α} {a : α}
 
 theorem isBounded_le_nhds (a : α) : (𝓝 a).IsBounded (· ≤ ·) :=
-  (isTop_or_exists_gt a).elim (fun h ↦ ⟨a, eventually_of_forall h⟩) fun ⟨b, hb⟩ ↦
-    ⟨b, ge_mem_nhds hb⟩
+  BoundedLENhdsClass.isBounded_le_nhds _
 #align is_bounded_le_nhds isBounded_le_nhds
 
-theorem Filter.Tendsto.isBoundedUnder_le {f : Filter β} {u : β → α} {a : α}
-    (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≤ ·) u :=
+theorem Filter.Tendsto.isBoundedUnder_le (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≤ ·) u :=
   (isBounded_le_nhds a).mono h
 #align filter.tendsto.is_bounded_under_le Filter.Tendsto.isBoundedUnder_le
 
-theorem Filter.Tendsto.bddAbove_range_of_cofinite {u : β → α} {a : α}
+theorem Filter.Tendsto.bddAbove_range_of_cofinite [IsDirected α (· ≤ ·)]
     (h : Tendsto u cofinite (𝓝 a)) : BddAbove (Set.range u) :=
   h.isBoundedUnder_le.bddAbove_range_of_cofinite
 #align filter.tendsto.bdd_above_range_of_cofinite Filter.Tendsto.bddAbove_range_of_cofinite
 
-theorem Filter.Tendsto.bddAbove_range {u : ℕ → α} {a : α} (h : Tendsto u atTop (𝓝 a)) :
-    BddAbove (Set.range u) :=
+theorem Filter.Tendsto.bddAbove_range [IsDirected α (· ≤ ·)] {u : ℕ → α}
+    (h : Tendsto u atTop (𝓝 a)) : BddAbove (Set.range u) :=
   h.isBoundedUnder_le.bddAbove_range
 #align filter.tendsto.bdd_above_range Filter.Tendsto.bddAbove_range
 
 theorem isCobounded_ge_nhds (a : α) : (𝓝 a).IsCobounded (· ≥ ·) :=
   (isBounded_le_nhds a).isCobounded_flip
 #align is_cobounded_ge_nhds isCobounded_ge_nhds
 
-theorem Filter.Tendsto.isCoboundedUnder_ge {f : Filter β} {u : β → α} {a : α} [NeBot f]
-    (h : Tendsto u f (𝓝 a)) : f.IsCoboundedUnder (· ≥ ·) u :=
+theorem Filter.Tendsto.isCoboundedUnder_ge [NeBot f] (h : Tendsto u f (𝓝 a)) :
+    f.IsCoboundedUnder (· ≥ ·) u :=
   h.isBoundedUnder_le.isCobounded_flip
 #align filter.tendsto.is_cobounded_under_ge Filter.Tendsto.isCoboundedUnder_ge
 
-end OrderClosedTopology
+instance : BoundedGENhdsClass αᵒᵈ := ⟨@isBounded_le_nhds α _ _ _⟩
 
-section OrderClosedTopology
+instance : BoundedLENhdsClass (α × β) := by
+  refine ⟨fun x ↦ ?_⟩
+  obtain ⟨a, ha⟩ := isBounded_le_nhds x.1
+  obtain ⟨b, hb⟩ := isBounded_le_nhds x.2
+  rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
+  exact ⟨(a, b), ha.prod_mk hb⟩
 
-variable [SemilatticeInf α] [TopologicalSpace α] [OrderTopology α]
+instance [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
+    [∀ i, BoundedLENhdsClass (π i)] : BoundedLENhdsClass (∀ i, π i) := by
+  refine' ⟨fun x ↦ _⟩
+  rw [nhds_pi]
+  choose f hf using fun i ↦ isBounded_le_nhds (x i)
+  exact ⟨f, eventually_pi hf⟩
+
+end BoundedLENhdsClass
+
+section BoundedGENhdsClass
+variable [BoundedGENhdsClass α] [BoundedGENhdsClass β] {f : Filter ι} {u : ι → α} {a : α}
 
 theorem isBounded_ge_nhds (a : α) : (𝓝 a).IsBounded (· ≥ ·) :=
-  isBounded_le_nhds (α := αᵒᵈ) a
+  BoundedGENhdsClass.isBounded_ge_nhds _
 #align is_bounded_ge_nhds isBounded_ge_nhds
 
-theorem Filter.Tendsto.isBoundedUnder_ge {f : Filter β} {u : β → α} {a : α}
-    (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≥ ·) u :=
+theorem Filter.Tendsto.isBoundedUnder_ge (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≥ ·) u :=
   (isBounded_ge_nhds a).mono h
 #align filter.tendsto.is_bounded_under_ge Filter.Tendsto.isBoundedUnder_ge
 
-theorem Filter.Tendsto.bddBelow_range_of_cofinite {u : β → α} {a : α}
+theorem Filter.Tendsto.bddBelow_range_of_cofinite [IsDirected α (· ≥ ·)]
     (h : Tendsto u cofinite (𝓝 a)) : BddBelow (Set.range u) :=
   h.isBoundedUnder_ge.bddBelow_range_of_cofinite
 #align filter.tendsto.bdd_below_range_of_cofinite Filter.Tendsto.bddBelow_range_of_cofinite
 
-theorem Filter.Tendsto.bddBelow_range {u : ℕ → α} {a : α} (h : Tendsto u atTop (𝓝 a)) :
-    BddBelow (Set.range u) :=
+theorem Filter.Tendsto.bddBelow_range [IsDirected α (· ≥ ·)] {u : ℕ → α}
+    (h : Tendsto u atTop (𝓝 a)) : BddBelow (Set.range u) :=
   h.isBoundedUnder_ge.bddBelow_range
 #align filter.tendsto.bdd_below_range Filter.Tendsto.bddBelow_range
 
 theorem isCobounded_le_nhds (a : α) : (𝓝 a).IsCobounded (· ≤ ·) :=
   (isBounded_ge_nhds a).isCobounded_flip
 #align is_cobounded_le_nhds isCobounded_le_nhds
 
-theorem Filter.Tendsto.isCoboundedUnder_le {f : Filter β} {u : β → α} {a : α} [NeBot f]
-    (h : Tendsto u f (𝓝 a)) : f.IsCoboundedUnder (· ≤ ·) u :=
+theorem Filter.Tendsto.isCoboundedUnder_le [NeBot f] (h : Tendsto u f (𝓝 a)) :
+    f.IsCoboundedUnder (· ≤ ·) u :=
   h.isBoundedUnder_ge.isCobounded_flip
 #align filter.tendsto.is_cobounded_under_le Filter.Tendsto.isCoboundedUnder_le
 
-end OrderClosedTopology
+instance : BoundedLENhdsClass αᵒᵈ := ⟨@isBounded_ge_nhds α _ _ _⟩
+
+instance : BoundedGENhdsClass (α × β) := by
+  refine ⟨fun x ↦ ?_⟩
+  obtain ⟨a, ha⟩ := isBounded_ge_nhds x.1
+  obtain ⟨b, hb⟩ := isBounded_ge_nhds x.2
+  rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
+  exact ⟨(a, b), ha.prod_mk hb⟩
+
+instance [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
+    [∀ i, BoundedGENhdsClass (π i)] : BoundedGENhdsClass (∀ i, π i) := by
+  refine' ⟨fun x ↦ _⟩
+  rw [nhds_pi]
+  choose f hf using fun i ↦ isBounded_ge_nhds (x i)
+  exact ⟨f, eventually_pi hf⟩
+
+end BoundedGENhdsClass
+
+-- See note [lower instance priority]
+instance (priority := 100) OrderTop.to_BoundedLENhdsClass [OrderTop α] : BoundedLENhdsClass α :=
+  ⟨fun _a ↦ isBounded_le_of_top⟩
+#align order_top.to_bounded_le_nhds_class OrderTop.to_BoundedLENhdsClass
+
+-- See note [lower instance priority]
+instance (priority := 100) OrderBot.to_BoundedGENhdsClass [OrderBot α] : BoundedGENhdsClass α :=
+  ⟨fun _a ↦ isBounded_ge_of_bot⟩
+#align order_bot.to_bounded_ge_nhds_class OrderBot.to_BoundedGENhdsClass
+
+-- See note [lower instance priority]
+instance (priority := 100) OrderTopology.to_BoundedLENhdsClass [IsDirected α (· ≤ ·)]
+    [OrderTopology α] : BoundedLENhdsClass α :=
+  ⟨fun a ↦
+    ((isTop_or_exists_gt a).elim fun h ↦ ⟨a, eventually_of_forall h⟩) <|
+      Exists.imp fun _b ↦ ge_mem_nhds⟩
+#align order_topology.to_bounded_le_nhds_class OrderTopology.to_BoundedLENhdsClass
+
+-- See note [lower instance priority]
+instance (priority := 100) OrderTopology.to_BoundedGENhdsClass [IsDirected α (· ≥ ·)]
+    [OrderTopology α] : BoundedGENhdsClass α :=
+  ⟨fun a ↦ ((isBot_or_exists_lt a).elim fun h ↦ ⟨a, eventually_of_forall h⟩) <|
+    Exists.imp fun _b ↦ le_mem_nhds⟩
+#align order_topology.to_bounded_ge_nhds_class OrderTopology.to_BoundedGENhdsClass
+
+end Preorder
+
+section LiminfLimsup
 
 section ConditionallyCompleteLinearOrder
 
@@ -258,7 +335,7 @@ end LiminfLimsup
 
 section Monotone
 
-variable {ι R S : Type*} {F : Filter ι} [NeBot F]
+variable {F : Filter ι} [NeBot F]
   [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
   [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S]
 
@@ -399,7 +476,7 @@ open Topology
 
 open Filter Set
 
-variable {ι : Type*} {R : Type*} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
+variable [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
 
 theorem iInf_eq_of_forall_le_of_tendsto {x : R} {as : ι → R} (x_le : ∀ i, x ≤ as i) {F : Filter ι}
     [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) : ⨅ i, as i = x := by
@@ -412,7 +489,7 @@ theorem iSup_eq_of_forall_le_of_tendsto {x : R} {as : ι → R} (le_x : ∀ i, a
   iInf_eq_of_forall_le_of_tendsto (R := Rᵒᵈ) le_x as_lim
 #align supr_eq_of_forall_le_of_tendsto iSup_eq_of_forall_le_of_tendsto
 
-theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
+theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
     {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) :
     ⋃ i : ι, Ici (as i) = Ioi x := by
   have obs : x ∉ range as := by
@@ -426,7 +503,7 @@ theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R}
   exact iUnion_Ici_eq_Ioi_iInf obs
 #align Union_Ici_eq_Ioi_of_lt_of_tendsto iUnion_Ici_eq_Ioi_of_lt_of_tendsto
 
-theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
+theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
     {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) :
     ⋃ i : ι, Iic (as i) = Iio x :=
   iUnion_Ici_eq_Ioi_of_lt_of_tendsto (R := Rᵒᵈ) x lt_x as_lim
@@ -512,10 +589,7 @@ theorem limsup_eq_tendsto_sum_indicator_atTop (R : Type*) [StrictOrderedSemiring
 end Indicator
 
 section LiminfLimsupAddSub
-
-set_option autoImplicit true
-
-variable {R : Type*} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
+variable [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
 
 /-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
 lemma limsup_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]