feat(topology/algebra/order/liminf_limsup): Eventual boundedness of n…

…eighborhoods (#18629)

Generalise `bounded_le_nhds`/`bounded_ge_nhds` using two ad hoc typeclasses. The goal here is to circumvent the fact that the product of order topologies is *not* an order topology, and apply those lemmas to `ℝⁿ`.

src/order/filter/pi.lean

@@ -28,6 +28,7 @@ open_locale classical filter
 namespace filter
 
 variables {ι : Type*} {α : ι → Type*} {f f₁ f₂ : Π i, filter (α i)} {s : Π i, set (α i)}
+  {p : Π i, α i → Prop}
 
 section pi
 
@@ -93,6 +94,14 @@ end
   I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i :=
 ⟨λ h i hi, mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩
 
+lemma 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
+
+lemma 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 $ λ i, (hf _).eval_pi
+
 lemma has_basis_pi {ι' : ι → Type} {s : Π i, ι' i → set (α i)} {p : Π i, ι' i → Prop}
   (h : ∀ i, (f i).has_basis (p i) (s i)) :
   (pi f).has_basis (λ If : set ι × Π i, ι' i, If.1.finite ∧ ∀ i ∈ If.1, p i (If.2 i))

src/topology/algebra/order/liminf_limsup.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 algebra.big_operators.intervals
 import algebra.big_operators.order
@@ -16,68 +16,152 @@ import topology.order.basic
 
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
 > Any changes to this file require a corresponding PR to mathlib4.
+
+## Main declarations
+
+* `bounded_le_nhds_class`: Typeclass stating that neighborhoods are eventually bounded above.
+* `bounded_ge_nhds_class`: Typeclass stating that neighborhoods are eventually bounded below.
+
+## Implementation notes
+
+The same lemmas are true in `ℝ`, `ℝ × ℝ`, `ι → ℝ`, `euclidean_space ι ℝ`. To avoid code
+duplication, we provide an ad hoc axiomatisation of the properties we need.
 -/
 
 open filter topological_space
 open_locale topology classical
 
 universes u v
-variables {α : Type u} {β : Type v}
+variables {ι α β R S : Type*} {π : ι → Type*}
 
-section liminf_limsup
+/-- Ad hoc typeclass stating that neighborhoods are eventually bounded above. -/
+class bounded_le_nhds_class (α : Type*) [preorder α] [topological_space α] : Prop :=
+(is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤))
+
+/-- Ad hoc typeclass stating that neighborhoods are eventually bounded below. -/
+class bounded_ge_nhds_class (α : Type*) [preorder α] [topological_space α] : Prop :=
+(is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥))
+
+section preorder
+variables [preorder α] [preorder β] [topological_space α] [topological_space β]
 
-section order_closed_topology
-variables [semilattice_sup α] [topological_space α] [order_topology α]
+section bounded_le_nhds_class
+variables [bounded_le_nhds_class α] [bounded_le_nhds_class β] {f : filter ι} {u : ι → α} {a : α}
 
 lemma is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤) :=
-(is_top_or_exists_gt a).elim (λ h, ⟨a, eventually_of_forall h⟩) (λ ⟨b, hb⟩, ⟨b, ge_mem_nhds hb⟩)
+bounded_le_nhds_class.is_bounded_le_nhds _
 
-lemma filter.tendsto.is_bounded_under_le {f : filter β} {u : β → α} {a : α}
-  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≤) u :=
+lemma filter.tendsto.is_bounded_under_le (h : tendsto u f (𝓝 a)) :
+  f.is_bounded_under (≤) u :=
 (is_bounded_le_nhds a).mono h
 
-lemma filter.tendsto.bdd_above_range_of_cofinite {u : β → α} {a : α}
+lemma filter.tendsto.bdd_above_range_of_cofinite [is_directed α (≤)]
   (h : tendsto u cofinite (𝓝 a)) : bdd_above (set.range u) :=
 h.is_bounded_under_le.bdd_above_range_of_cofinite
 
-lemma filter.tendsto.bdd_above_range {u : ℕ → α} {a : α}
-  (h : tendsto u at_top (𝓝 a)) : bdd_above (set.range u) :=
+lemma filter.tendsto.bdd_above_range [is_directed α (≤)] {u : ℕ → α} (h : tendsto u at_top (𝓝 a)) :
+  bdd_above (set.range u) :=
 h.is_bounded_under_le.bdd_above_range
 
 lemma is_cobounded_ge_nhds (a : α) : (𝓝 a).is_cobounded (≥) :=
 (is_bounded_le_nhds a).is_cobounded_flip
 
-lemma filter.tendsto.is_cobounded_under_ge {f : filter β} {u : β → α} {a : α}
-  [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≥) u :=
+lemma filter.tendsto.is_cobounded_under_ge [ne_bot f] (h : tendsto u f (𝓝 a)) :
+  f.is_cobounded_under (≥) u :=
 h.is_bounded_under_le.is_cobounded_flip
 
-end order_closed_topology
+instance : bounded_ge_nhds_class αᵒᵈ := ⟨@is_bounded_le_nhds α _ _ _⟩
+
+instance : bounded_le_nhds_class (α × β) :=
+begin
+  refine ⟨λ x, _⟩,
+  obtain ⟨a, ha⟩ := is_bounded_le_nhds x.1,
+  obtain ⟨b, hb⟩ := is_bounded_le_nhds x.2,
+  rw [←@prod.mk.eta _ _ x, nhds_prod_eq],
+  exact ⟨(a, b), ha.prod_mk hb⟩,
+end
+
+instance [finite ι] [Π i, preorder (π i)] [Π i, topological_space (π i)]
+  [Π i, bounded_le_nhds_class (π i)] : bounded_le_nhds_class (Π i, π i) :=
+begin
+  refine ⟨λ x, _⟩,
+  rw nhds_pi,
+  choose f hf using λ i, is_bounded_le_nhds (x i),
+  exact ⟨f, eventually_pi hf⟩,
+end
+
+end bounded_le_nhds_class
 
-section order_closed_topology
-variables [semilattice_inf α] [topological_space α] [order_topology α]
+section bounded_ge_nhds_class
+variables [bounded_ge_nhds_class α] [bounded_ge_nhds_class β] {f : filter ι} {u : ι → α} {a : α}
 
-lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) := @is_bounded_le_nhds αᵒᵈ _ _ _ a
+lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) :=
+bounded_ge_nhds_class.is_bounded_ge_nhds _
 
-lemma filter.tendsto.is_bounded_under_ge {f : filter β} {u : β → α} {a : α}
-  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≥) u :=
+lemma filter.tendsto.is_bounded_under_ge (h : tendsto u f (𝓝 a)) :
+  f.is_bounded_under (≥) u :=
 (is_bounded_ge_nhds a).mono h
 
-lemma filter.tendsto.bdd_below_range_of_cofinite {u : β → α} {a : α}
+lemma filter.tendsto.bdd_below_range_of_cofinite [is_directed α (≥)]
   (h : tendsto u cofinite (𝓝 a)) : bdd_below (set.range u) :=
 h.is_bounded_under_ge.bdd_below_range_of_cofinite
 
-lemma filter.tendsto.bdd_below_range {u : ℕ → α} {a : α}
-  (h : tendsto u at_top (𝓝 a)) : bdd_below (set.range u) :=
+lemma filter.tendsto.bdd_below_range [is_directed α (≥)] {u : ℕ → α} (h : tendsto u at_top (𝓝 a)) :
+  bdd_below (set.range u) :=
 h.is_bounded_under_ge.bdd_below_range
 
 lemma is_cobounded_le_nhds (a : α) : (𝓝 a).is_cobounded (≤) :=
 (is_bounded_ge_nhds a).is_cobounded_flip
 
-lemma filter.tendsto.is_cobounded_under_le {f : filter β} {u : β → α} {a : α}
-  [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≤) u :=
+lemma filter.tendsto.is_cobounded_under_le [ne_bot f] (h : tendsto u f (𝓝 a)) :
+  f.is_cobounded_under (≤) u :=
 h.is_bounded_under_ge.is_cobounded_flip
 
-end order_closed_topology
+instance : bounded_le_nhds_class αᵒᵈ := ⟨@is_bounded_ge_nhds α _ _ _⟩
+
+instance : bounded_ge_nhds_class (α × β) :=
+begin
+  refine ⟨λ x, _⟩,
+  obtain ⟨a, ha⟩ := is_bounded_ge_nhds x.1,
+  obtain ⟨b, hb⟩ := is_bounded_ge_nhds x.2,
+  rw [←@prod.mk.eta _ _ x, nhds_prod_eq],
+  exact ⟨(a, b), ha.prod_mk hb⟩,
+end
+
+instance [finite ι] [Π i, preorder (π i)] [Π i, topological_space (π i)]
+  [Π i, bounded_ge_nhds_class (π i)] : bounded_ge_nhds_class (Π i, π i) :=
+begin
+  refine ⟨λ x, _⟩,
+  rw nhds_pi,
+  choose f hf using λ i, is_bounded_ge_nhds (x i),
+  exact ⟨f, eventually_pi hf⟩,
+end
+
+end bounded_ge_nhds_class
+
+@[priority 100] -- See note [lower instance priority]
+instance order_top.to_bounded_le_nhds_class [order_top α] : bounded_le_nhds_class α :=
+⟨λ a, is_bounded_le_of_top⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_bot.to_bounded_ge_nhds_class [order_bot α] : bounded_ge_nhds_class α :=
+⟨λ a, is_bounded_ge_of_bot⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_topology.to_bounded_le_nhds_class [is_directed α (≤)] [order_topology α] :
+  bounded_le_nhds_class α :=
+⟨λ a, (is_top_or_exists_gt a).elim (λ h, ⟨a, eventually_of_forall h⟩) $ Exists.imp $ λ b,
+  ge_mem_nhds⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_topology.to_bounded_ge_nhds_class [is_directed α (≥)] [order_topology α] :
+  bounded_ge_nhds_class α :=
+⟨λ a, (is_bot_or_exists_lt a).elim (λ h, ⟨a, eventually_of_forall h⟩) $ Exists.imp $ λ b,
+  le_mem_nhds⟩
+
+end preorder
+
+section liminf_limsup
 
 section conditionally_complete_linear_order
 variables [conditionally_complete_linear_order α]
@@ -224,7 +308,7 @@ end liminf_limsup
 
 section monotone
 
-variables {ι R S : Type*} {F : filter ι} [ne_bot F]
+variables {F : filter ι} [ne_bot F]
   [complete_linear_order R] [topological_space R] [order_topology R]
   [complete_linear_order S] [topological_space S] [order_topology S]
 
@@ -334,7 +418,7 @@ open_locale topology
 
 open filter set
 
-variables {ι : Type*} {R : Type*} [complete_linear_order R] [topological_space R] [order_topology R]
+variables [complete_linear_order R] [topological_space R] [order_topology R]
 
 lemma infi_eq_of_forall_le_of_tendsto {x : R} {as : ι → R}
   (x_le : ∀ i, x ≤ as i) {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
@@ -349,7 +433,7 @@ lemma supr_eq_of_forall_le_of_tendsto {x : R} {as : ι → R}
   (⨆ i, as i) = x :=
 @infi_eq_of_forall_le_of_tendsto ι (order_dual R) _ _ _ x as le_x F _ as_lim
 
-lemma Union_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
+lemma Union_Ici_eq_Ioi_of_lt_of_tendsto (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
   {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
   (⋃ (i : ι), Ici (as i)) = Ioi x :=
 begin
@@ -361,10 +445,10 @@ begin
   exact Union_Ici_eq_Ioi_infi obs,
 end
 
-lemma Union_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
+lemma Union_Iic_eq_Iio_of_lt_of_tendsto (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
   {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
   (⋃ (i : ι), Iic (as i)) = Iio x :=
-@Union_Ici_eq_Ioi_of_lt_of_tendsto (order_dual R) _ _ _ ι x as lt_x F _ as_lim
+@Union_Ici_eq_Ioi_of_lt_of_tendsto ι Rᵒᵈ _ _ _ _ _ lt_x F _ as_lim
 
 end infi_and_supr