feat: generalize cocompact_eq (#10285)

example use case: `cocompact_le` with `integrable_iff_integrableAtFilter_cocompact` from #10248 becomes a way to prove integrability from big-O estimates (e.g. #10258)



Co-authored-by: L Lllvvuu <git@llllvvuu.dev>

Mathlib/Analysis/Complex/PhragmenLindelof.lean

@@ -710,7 +710,7 @@ theorem right_half_plane_of_tendsto_zero_on_real (hd : DiffContOnCl ℂ f {z | 0
     have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff]
     suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by
       simpa only [exists_prop] using hfc.norm.exists_forall_ge' isClosed_Ici hx₀ this
-    rw [Real.cocompact_eq, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot,
+    rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot,
       bot_sup_eq]
     exact (hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left
   rcases le_or_lt ‖f x₀‖ C with h | h

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -195,7 +195,7 @@ theorem isBigO_norm_restrict_cocompact (f : C(ℝ, E)) {b : ℝ} (hb : 0 < b)
     refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, _⟩)
     · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
     · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
-  simp_rw [cocompact_eq, isBigO_sup] at hf ⊢
+  simp_rw [cocompact_eq_atBot_atTop, isBigO_sup] at hf ⊢
   constructor
   · refine' (isBigO_of_le atBot _).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
     simp_rw [norm_norm]; exact this

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

@@ -633,7 +633,7 @@ lemma cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ
 
 lemma cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
     (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[cocompact ℝ] (|·| ^ s) := by
-  rw [Real.cocompact_eq, isLittleO_sup]
+  rw [cocompact_eq_atBot_atTop, isLittleO_sup]
   constructor
   · refine ((cexp_neg_quadratic_isLittleO_rpow_atTop ha (-b) s).comp_tendsto
       Filter.tendsto_neg_atBot_atTop).congr' (eventually_of_forall fun x ↦ ?_) ?_
@@ -647,7 +647,7 @@ lemma cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0)
 theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) :
     Tendsto (fun x : ℝ => |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0) := by
   conv in rexp _ => rw [← sq_abs]
-  erw [cocompact_eq, ← comap_abs_atTop,
+  erw [cocompact_eq_atBot_atTop, ← comap_abs_atTop,
     @tendsto_comap'_iff _ _ _ (fun y => y ^ s * rexp (-a * y ^ 2)) _ _ _
       (mem_atTop_sets.mpr ⟨0, fun b hb => ⟨b, abs_of_nonneg hb⟩⟩)]
   exact

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -579,6 +579,13 @@ instance atBot_isMeasurablyGenerated : (Filter.atBot : Filter α).IsMeasurablyGe
     (measurableSet_Iic : MeasurableSet (Iic a)).principal_isMeasurablyGenerated
 #align at_bot_is_measurably_generated atBot_isMeasurablyGenerated
 
+instance [R1Space α] : IsMeasurablyGenerated (cocompact α) where
+  exists_measurable_subset := by
+    intro _ hs
+    obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
+    exact ⟨(closure t)ᶜ, ht.closure.compl_mem_cocompact, isClosed_closure.measurableSet.compl,
+      (compl_subset_compl.2 subset_closure).trans hts⟩
+
 end Preorder
 
 section PartialOrder

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -707,7 +707,7 @@ theorem _root_.HasCompactSupport.integral_Ioi_deriv_eq (hf : ContDiff ℝ 1 f)
   rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub]
   refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn
   rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f
-  exact h2f.filter_mono atTop_le_cocompact |>.tendsto
+  exact h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto
 
 /-- When a function has a limit at infinity, and its derivative is nonnegative, then the derivative
 is automatically integrable on `(a, +∞)`. Version assuming differentiability
@@ -857,7 +857,7 @@ theorem _root_.HasCompactSupport.integral_Iic_deriv_eq (hf : ContDiff ℝ 1 f)
   rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero]
   refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn
   rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f
-  exact h2f.filter_mono atBot_le_cocompact |>.tendsto
+  exact h2f.filter_mono _root_.atBot_le_cocompact |>.tendsto
 
 end IicFTC
 

Mathlib/Topology/Algebra/Order/Compact.lean

@@ -65,6 +65,12 @@ lemma CompactIccSpace.mk'' [TopologicalSpace α] [PartialOrder α]
     (h : ∀ {a b : α}, a < b → IsCompact (Icc a b)) : CompactIccSpace α :=
   .mk' fun hab => hab.eq_or_lt.elim (by rintro rfl; simp) h
 
+instance [TopologicalSpace α] [Preorder α] [CompactIccSpace α] : CompactIccSpace (αᵒᵈ) where
+  isCompact_Icc := by
+    intro a b
+    convert isCompact_Icc (α := α) (a := b) (b := a) using 1
+    exact dual_Icc (α := α)
+
 /-- A closed interval in a conditionally complete linear order is compact. -/
 instance (priority := 100) ConditionallyCompleteLinearOrder.toCompactIccSpace (α : Type*)
     [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] :
@@ -193,6 +199,63 @@ theorem IsCompact.exists_isLUB [ClosedIciTopology α] {s : Set α} (hs : IsCompa
   IsCompact.exists_isGLB (α := αᵒᵈ) hs ne_s
 #align is_compact.exists_is_lub IsCompact.exists_isLUB
 
+theorem cocompact_le_atBot_atTop [LinearOrder α] [CompactIccSpace α] :
+    cocompact α ≤ atBot ⊔ atTop := by
+  refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
+  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
+  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1
+    obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
+    refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
+    exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_le h)) fun h ↦ hu x (le_of_not_le h)
+
+theorem cocompact_le_atBot [LinearOrder α] [OrderTop α] [CompactIccSpace α] :
+    cocompact α ≤ atBot := by
+  refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
+  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
+  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
+    refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
+    exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_le h)) (fun h ↦ (h le_top).elim)
+
+theorem cocompact_le_atTop [LinearOrder α] [OrderBot α] [CompactIccSpace α] :
+    cocompact α ≤ atTop :=
+  cocompact_le_atBot (α := αᵒᵈ)
+
+theorem atBot_le_cocompact [LinearOrder α] [NoMinOrder α] [ClosedIicTopology α] :
+    atBot ≤ cocompact α := by
+  refine fun s hs ↦ ?_
+  obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
+  refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)
+  · rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts
+    convert univ_mem
+  · haveI := h_nonempty.nonempty
+    obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty
+    obtain ⟨b, hb⟩ := exists_lt a
+    exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
+      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_not_mem.mp hc)⟩
+
+theorem atTop_le_cocompact [LinearOrder α] [NoMaxOrder α] [ClosedIciTopology α] :
+    atTop ≤ cocompact α :=
+  atBot_le_cocompact (α := αᵒᵈ)
+
+theorem atBot_atTop_le_cocompact [LinearOrder α] [NoMinOrder α] [NoMaxOrder α]
+    [OrderClosedTopology α] : atBot ⊔ atTop ≤ cocompact α :=
+  sup_le atBot_le_cocompact atTop_le_cocompact
+
+@[simp 900]
+theorem cocompact_eq_atBot_atTop [LinearOrder α] [NoMaxOrder α] [NoMinOrder α]
+    [OrderClosedTopology α] [CompactIccSpace α] : cocompact α = atBot ⊔ atTop :=
+  cocompact_le_atBot_atTop.antisymm atBot_atTop_le_cocompact
+
+@[simp]
+theorem cocompact_eq_atBot [LinearOrder α] [NoMinOrder α] [OrderTop α]
+    [ClosedIicTopology α] [CompactIccSpace α] : cocompact α = atBot :=
+  cocompact_le_atBot.antisymm atBot_le_cocompact
+
+@[simp]
+theorem cocompact_eq_atTop [LinearOrder α] [NoMaxOrder α] [OrderBot α]
+    [ClosedIciTopology α] [CompactIccSpace α] : cocompact α = atTop :=
+  cocompact_le_atTop.antisymm atTop_le_cocompact
+
 -- porting note: new lemma; defeq to the old one but allows us to use dot notation
 /-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/
 theorem IsCompact.exists_isMinOn [ClosedIicTopology α] {s : Set β} (hs : IsCompact s)

Mathlib/Topology/Compactness/Compact.lean

@@ -570,7 +570,8 @@ theorem cocompact_eq_cofinite (X : Type*) [TopologicalSpace X] [DiscreteTopology
   simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]
 #align filter.cocompact_eq_cofinite Filter.cocompact_eq_cofinite
 
-@[simp] theorem _root_.Nat.cocompact_eq : cocompact ℕ = atTop :=
+-- deprecated on 2024-02-07: see `cocompact_eq_atTop` with `import Mathlib.Topology.Instances.Nat`
+@[deprecated] theorem _root_.Nat.cocompact_eq : cocompact ℕ = atTop :=
   (cocompact_eq_cofinite ℕ).trans Nat.cofinite_eq_atTop
 #align nat.cocompact_eq Nat.cocompact_eq
 

Mathlib/Topology/Instances/Int.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Data.Int.Interval
-import Mathlib.Topology.MetricSpace.Basic
-import Mathlib.Topology.MetricSpace.PseudoMetric
+import Mathlib.Data.Int.SuccPred
+import Mathlib.Data.Int.ConditionallyCompleteOrder
+import Mathlib.Topology.Instances.Discrete
 import Mathlib.Topology.MetricSpace.Bounded
 import Mathlib.Order.Filter.Archimedean
 
@@ -76,14 +77,12 @@ theorem cobounded_eq : Bornology.cobounded ℤ = atBot ⊔ atTop := by
   simp_rw [← comap_dist_right_atTop (0 : ℤ), dist_eq', sub_zero,
     ← comap_abs_atTop, ← @Int.comap_cast_atTop ℝ, comap_comap]; rfl
 
-@[simp]
-theorem cocompact_eq : cocompact ℤ = atBot ⊔ atTop := by
-  rw [← cobounded_eq_cocompact, cobounded_eq]
+@[deprecated] alias cocompact_eq := cocompact_eq_atBot_atTop -- deprecated on 2024-02-07
 #align int.cocompact_eq Int.cocompact_eq
 
 @[simp]
 theorem cofinite_eq : (cofinite : Filter ℤ) = atBot ⊔ atTop := by
-  rw [← cocompact_eq_cofinite, cocompact_eq]
+  rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]
 #align int.cofinite_eq Int.cofinite_eq
 
 end Int

Mathlib/Topology/Instances/Real.lean

@@ -74,13 +74,11 @@ theorem Real.isTopologicalBasis_Ioo_rat :
 theorem Real.cobounded_eq : cobounded ℝ = atBot ⊔ atTop := by
   simp only [← comap_dist_right_atTop (0 : ℝ), Real.dist_eq, sub_zero, comap_abs_atTop]
 
-@[simp]
-theorem Real.cocompact_eq : cocompact ℝ = atBot ⊔ atTop := by
-  rw [← cobounded_eq_cocompact, cobounded_eq]
+@[deprecated] alias Real.cocompact_eq := cocompact_eq_atBot_atTop
 #align real.cocompact_eq Real.cocompact_eq
 
-theorem Real.atBot_le_cocompact : atBot ≤ cocompact ℝ := by simp
-theorem Real.atTop_le_cocompact : atTop ≤ cocompact ℝ := by simp
+@[deprecated] alias Real.atBot_le_cocompact := atBot_le_cocompact -- deprecated on 2024-02-07
+@[deprecated] alias Real.atTop_le_cocompact := atBot_le_cocompact -- deprecated on 2024-02-07
 
 /- TODO(Mario): Prove that these are uniform isomorphisms instead of uniform embeddings
 lemma uniform_embedding_add_rat {r : ℚ} : uniform_embedding (fun p : ℚ => p + r) :=